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# 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"
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
