[isabelle-dev] Option type for auto tools timeout

[David Aspinall]

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!)

  - D.

-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.