*To*: isabelle-users at cl.cam.ac.uk, nipkow at in.tum.de, alfio.martini at acm.org*Subject*: Re: [isabelle] Isabelle/jedit*From*: Fabian Immler <immler at in.tum.de>*Date*: Sun, 22 Jul 2012 19:42:07 +0200*In-reply-to*: <CAAPnxw2wxZbTW5pCNrXxqs+D7voO=nqLvEp89Lkf_+GGXdUh-w@mail.gmail.com>*References*: <500BDE34.8030100@in.tum.de> <CAAPnxw2wxZbTW5pCNrXxqs+D7voO=nqLvEp89Lkf_+GGXdUh-w@mail.gmail.com>*Sender*: fabian.immler at gmail.com

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

**Attachment:
update.bsh**

**Follow-Ups**:**Re: [isabelle] Isabelle/jedit***From:*Christian Sternagel

**Re: [isabelle] Isabelle/jedit***From:*Tobias Nipkow

**References**:**[isabelle] Isabelle/jedit***From:*Tobias Nipkow

**Re: [isabelle] Isabelle/jedit***From:*Alfio Martini

- Previous by Date: Re: [isabelle] Changing the arity of a term in ML
- Next by Date: Re: [isabelle] Schematic vars or universal bound vars in theorem?
- Previous by Thread: Re: [isabelle] Isabelle/jedit
- Next by Thread: Re: [isabelle] Isabelle/jedit
- Cl-isabelle-users July 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list