[isabelle-dev] Option type for auto tools timeout
David.Aspinall at ed.ac.uk
Tue Jan 11 18:10:22 CET 2011
On 11/01/11 16:37, Makarius wrote:
> 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")
Hmm. The widget type is different to the elisp type. Nuisance. Have
adjusted that patch.
> 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.
I think 4 files if you add separate input validation for the new type
(deffloatset) which I didn't. Have done now but not tested...
> 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.
Thanks -- unfortunately not geared for building atm.
Can you try again now and send me stacktrace of a bug if you get it and
I've still missed something? (Off list!)
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
More information about the isabelle-dev