Re: [isabelle] Isabelle/jedit

2012/7/23 Tobias Nipkow <nipkow at>:
> 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.
Try the attached macro!

> 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>:
>>> 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> 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

Attachment: auto_update.bsh
Description: Binary data

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