[isabelle-dev] Option type for auto tools timeout

[Makarius]

On Tue, 11 Jan 2011, David Aspinall wrote:

>
>> (error "defpacustom: missing :type keyword or wrong :type value")
>
> Thanks -- just patched pg-pamacs.el which should fix.  Can you re-try?

Now the error is:

   (error "Invalid menu item in easymenu")

I've already tried myself to look through all the occurrences of 'integer 
and add a analogous 'float versions.  This turned out to affect approx. 5 
files, when I gave up.

Included is a tiny changeset to activate the pgipfloat protocol message on 
the Isabelle side, so you can see yourself.  You need to build HOL-Plain 
at the least, which is a bit faster than full HOL.


 	Makarius
-------------- next part --------------
# HG changeset patch
# User wenzelm
# Date 1294763673 -3600
# Node ID 6f7efa7dc4e0e5141fbd3ab80c941dd771c2f54e
# Parent  f1e7e244dcf5bdeb25b5340845c5dc6f7edf1a15
actually emit pgipfloat message;

diff -r f1e7e244dcf5 -r 6f7efa7dc4e0 src/Pure/ProofGeneral/pgip_types.ML
--- a/src/Pure/ProofGeneral/pgip_types.ML	Tue Jan 11 17:00:21 2011 +0100
+++ b/src/Pure/ProofGeneral/pgip_types.ML	Tue Jan 11 17:34:33 2011 +0100
@@ -272,7 +272,7 @@
                     | Pgipbool => "pgipbool"
                     | Pgipint _ => "pgipint"
                     | Pgipnat => "pgipint"
-                    | Pgipreal => "pgipint"  (* FIXME sic? *)
+                    | Pgipreal => "pgipfloat"
                     | Pgipstring => "pgipstring"
                     | Pgipconst _ => "pgipconst"
                     | Pgipchoice _ => "pgipchoice"