[isabelle-dev] Proof General 4.1pre

[Makarius]

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