Re: [isabelle] Isabelle/jedit
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"
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
- 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
- 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 acm.org>:
Dear Isabelle Users
I am also interested in a possible answer to this question. What I
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 in.tum.de> wrote:
When I start typing in a proof command, eg apply, jedit eagerly executes
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