Re: [isabelle] Isabelle/jedit

Dear all,

I was going to suggest an alternative to Fabian's setup where we could use a keyboard shortcut to toggle "Auto update". My idea was that you turn "Auto update" off in situations where you want to have a look at the current proof state while typing the next method application (which is not always the case since often subgoals are easy enough that we do not really have to think about them) and afterwards turn "Auto update" on again.

However, when trying this (currently by manually clicking on the "Auto update" checkbox of the "Output" panel) I noticed what I would consider undesirable behavior which I will illustrate by the following example (where [...] indicates the cursor position):

  lemma "A & B --> B & A"[]

At this point we have the subgoal

   1. A ∧ B ⟶ B ∧ A

Now I turn off "Auto update" and type Enter to go to the next line. Unfortunately, even with "Auto update" turned off, the "Output" panel is "updated" to an empty state. The same happens when starting from

  lamme "A & B --> B & A"

and typing anything (already in the new line). Wouldn't it be preferable if "Output" would not change at all, after switching off "Auto update"?



On 07/23/2012 02:42 AM, Fabian Immler wrote:
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).


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
way to see the old proof state while I type the proof command?


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.