*To*: Vadim Zaliva <vzaliva at cmu.edu>*Subject*: Re: [isabelle] Isabelle 2014 and proof general*From*: Makarius <makarius at sketis.net>*Date*: Fri, 12 Sep 2014 18:12:45 +0200 (CEST)*Cc*: Isabelle Users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DDAA61EE-A860-43B5-B803-1AC5A98D3675@cmu.edu>*References*: <A216A54B-BD72-4913-ADE9-B545E83D0813@cmu.edu> <alpine.LNX.2.00.1409102031580.41896@lxbroy10.informatik.tu-muenchen.de> <DDAA61EE-A860-43B5-B803-1AC5A98D3675@cmu.edu>*User-agent*: Alpine 2.00 (LNX 1167 2008-08-23)

On Fri, 12 Sep 2014, Vadim Zaliva wrote:

Let me put forward some arguments in defence of Proof General support inIsabelle.

For the purpose of this discussion the functionality of PIDE such asProof General as well as Isabelle/Jedit could be broadly split into 3categories:1. Basic functionality - basic editing functionality used in Isabelle mode as well as for other modes. Here you have managing multiple buffers, windows, search, clipboard, completion, etc. 2. Isabelle specific interface. 3. Other functionality of the PIDE which is not strictly speaking is necessary for working with Isabelle. For example integration with other languages (ML, LISP, Haskell), spell checker integration, etc.

I have limited experience with #2 but for my purposes both Proof Generaland Isabelle/JEdit were comparable.

Some people might find Jedit/Isabelle asynchronous proving superior toProof General's sequential mode but I like the control Proof Generalgives me.

The document-oriented approach with implicit checking is inherent in PIDE.

Most importantly in #1 I found jEdit (mind you, not Isabelle/jEdit butjEdit itself) lacking, compared to Emacs. A couple of trivial examples:I-search and working with rectangular blocks in copy/paste.

Finally, although it is not directly related to Isabelle, I think in #3emacs have much more to offer due to the amount of code written forEmacs over the decades.

For example I am working with Haskell, LISP code and Isabelle proofs atthe same time and now I am forced to run jEdit and Emacs concurrently.Emacs key binding in jEdit are not exactly the same as real Emacs on Macso I am constantly struggling when switching between the two. With ProofGeneral I was easily editing all Isabelle, LISP and Haskell from thecomfort of the same familiar environment.

Makarius

**References**:**[isabelle] Isabelle 2014 and proof general***From:*Vadim Zaliva

**Re: [isabelle] Isabelle 2014 and proof general***From:*Makarius

**Re: [isabelle] Isabelle 2014 and proof general***From:*Vadim Zaliva

- Previous by Date: Re: [isabelle] How to use latex commands inside proof?
- Next by Date: Re: [isabelle] Isabelle 2014 and proof general
- Previous by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Next by Thread: Re: [isabelle] Isabelle 2014 and proof general
- Cl-isabelle-users September 2014 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