[isabelle-dev] Option type for auto tools timeout

[David Aspinall]

> The Proof General protocol does not understand pgreal, but happens to
> interpret a pgint value in a way that accepts floating point numbers as
> well -- the target language is Emacs LISP where everything is untyped
> anyway.

This is (partially) true for the PGIP implementation in Emacs, but not 
true for the Java and Haskell implementations of PGIP, and not true for 
the XML Schema that defines the message format.

PGIP is supposed to be a typed protocol.  There perhaps aren't many 
users of those other tools which check messages strictly, but it would 
be better to upgrade the protocol rather than break it crudely.

  - David

PS it seems like a fine time to do this, a patch in Proof General would 
be easy and a 4.1 release will be made soon to support latest Coq.

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.