Re: [isabelle] Isabelle/jedit



Thank you, that was very helpful, I have installed your macro and will try it
out. Christian's idea of toggling Auto update sounds interesting, too, but I
would need a macro to try it.

This brings me to the next issue. Not updating the output panel does not keep
the prover from evaluating my partially edited proof text in the background. But
since I have edited the beginning of the text, the rest often does not make
sense anymore, or the parser parses it in an unintended way, at least up to the
next synchronisation point like "lemma". Frequently this leads to diverging
proof steps a bit further down, which are shown in purple. Together with the fan
coming on this is a bit distracting and I often feel compelled to comment out
bits of the proof in response. Is there any way to control the over-eager
evaluation to avoid such situations?

Thanks!
Tobias

Am 22/07/2012 19:42, schrieb Fabian Immler:
> You could disable "Auto update" in the Output panel and use "Update" manually.
> 
> Since "Update" is not exported as an action of the Isabelle-Plugin,
> one cannot assign a keyboard shortcut to see the current proof state.
> 
> The attached macro (a short hack) emulates a click on "Update" and
> could be used for an alternative way of interaction:
> - No "Auto update"
> - Keyboard shortcut (e.g. Ctrl-Enter) to see the current proof state
> 
> Installation instructions:
>  - Move the attached update.bsh to
> ~/.isabelle/Isabelle2012/jedit/macros/ (This script "clicks" on
> "Update")
>  - Assign a shortcut to this Macro:
>     - either via Utilities->Global Options->Shortcuts (The macro is
> called "update")
>     - or by appending a line like "update.shortcut=A+ENTER A+m" to
> ~/.isabelle/Isabelle2012/jedit/properties
> 
> If this turns out to be a desired/competitive way of interaction, one
> could think about having these actions exported by the
> Isabelle-Plugin.
> 
> Now trying to prove theorems with manual updates of the proof state,
> Fabian
> 
> 2012/7/22 Alfio Martini <alfio.martini at acm.org>:
>> Dear Isabelle Users
>>
>> I am also  interested in  a possible answer to this question. What I
>> usually do
>> in this case is to [repeatedly] move the cursor to the previous [next] line
>> (command, declaration) to take
>> a look  at the current proof state before resuming
>> typing or thinking about the current command (declaration).
>>
>> Cheers
>>
>> On Sun, Jul 22, 2012 at 8:04 AM, Tobias Nipkow <nipkow at in.tum.de> wrote:
>>
>>> When I start typing in a proof command, eg apply, jedit eagerly executes
>>> it, and
>>> since I am in the middle of typing it, the command typically fails.
>>> Unfortunately the resulting error msg overwrites the proof state. Is there
>>> any
>>> way to see the old proof state while I type the proof command?
>>>
>>> Thanks
>>> Tobias
>>>
>>>
>>
>>
>> --
>> Alfio Ricardo Martini
>> PhD in Computer Science (TU Berlin)
>> Associate Professor at Faculty of Informatics (PUCRS)
>> Coordenador do Curso de Ciência da Computação
>> Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
>> 90619-900 -Porto Alegre - RS - Brasil





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.