[isabelle-dev] Proof General 4.1pre
makarius at sketis.net
Fri Jan 14 16:59:07 CET 2011
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 188.8.131.52 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.
More information about the isabelle-dev