On Thu, 13 Jan 2011, Makarius wrote:
If there is the slightest doubt we can also keep the odd treatment of
pgreal values in Isabelle2011 -- PG 4.1 would work nonetheless, despite
our abuse of the protocol.
I would say that sufficient doubts have accumulated. So we stick to the
"embrace-and-extend" version of PGIP in Isabelle2011.
PG 3.7.x, 4.0 and 4.1 should all work with that.
On Thu, 23 Dec 2010, Holger Gast wrote:
It seems easy enough to make the necessary change on the Isabelle side
the relevant line in pgip_types.ML (ba13793594f0) has a "FIXME"
annotation already. If Emacs PG 3.7.1.1 disregards the type information
anyway and 4.0 will use it, it would perhaps be nice to follow David's
proposal for consistency's sake.
If this will not happen, just let me know -- I3P will simply substitute
the correct type for the particular parameter silently depending on the
Isabelle version.
Yes, "pgint" messages can contain floating point text, as before. So any
Proof General clones need to cope with that.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
