[isabelle-dev] Option type for auto tools timeout

[Holger Gast]

> On Wed, 15 Dec 2010, David Aspinall wrote:
> 
>> 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.
> 
> In the classic time of Proof General I always spent a lot of creativity
> on extending the functionality of the prover without breaking the
> protocol. This has become increasingly difficult, and the protocol has
> legacy status for many years already, so I stopped such extra efforts at
> some point.

>> 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.
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.

Thanks,

Holger