*To*: Markus Wenzel <makarius at sketis.net>*Subject*: Re: [isabelle] Remaining reasons for Proof General*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 11 Nov 2013 15:39:18 +0000*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*In-reply-to*: <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de>*References*: <CANofLeJJ8O2Y2ktXUER1AsH1F4CQsBB21PPbLMVVQa-UfwjgoQ@mail.gmail.com> <353FF788-2AA0-4188-8AAD-28E803A1F647@gmail.com> <CANofLeLVT7QWSUE4HhNy+kq9UuCe4J7gsXVEzma0x_SO5C03wQ@mail.gmail.com> <26755B7F-E696-4A5D-9BE7-9BCFA0FF85B8@gmail.com> <alpine.LNX.2.00.1311111227510.20958@macbroy21.informatik.tu-muenchen.de> <5280E51C.3010703@inf.ethz.ch> <alpine.LNX.2.00.1311111531350.10735@macbroy21.informatik.tu-muenchen.de>

You can put any number of marks in a file. They track edits quite well, and they persist over sessions. Larry On 11 Nov 2013, at 14:59, Makarius <makarius at sketis.net> wrote: >> Similarly, I often want to look somewhere else in my theory file (and use PgUp/PgDn for that); with ProofGeneral, I just type C-c C-. to get back to where I was before, but I do not know an equally simple way in jEdit. > > ... > What jEdit (or Isabelle/jEdit) really needs is nice navigation support in the sense of Firefox or similar. One mainly needs to work out a good scheme when or how to "commit" positions to the navigation history, and maybe brush up the existing Navigator plugin.

**Follow-Ups**:**Re: [isabelle] Remaining reasons for Proof General***From:*Makarius

**References**:**[isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Randy Pollack

**Re: [isabelle] sledgehammer in RC4***From:*Jasmin Blanchette

**Re: [isabelle] sledgehammer in RC4***From:*Makarius

**Re: [isabelle] sledgehammer in RC4***From:*Andreas Lochbihler

**[isabelle] Remaining reasons for Proof General***From:*Makarius

- Previous by Date: [isabelle] Remaining reasons for Proof General
- Next by Date: Re: [isabelle] Remaining reasons for Proof General
- Previous by Thread: [isabelle] Remaining reasons for Proof General
- Next by Thread: Re: [isabelle] Remaining reasons for Proof General
- Cl-isabelle-users November 2013 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