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.
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
