Re: [isabelle] Isabelle/jedit

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

If this turns out to be a desired/competitive way of interaction, one
could think about having these actions exported by the

Now trying to prove theorems with manual updates of the proof state,

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: update.bsh
Description: Binary data

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