[isabelle-dev] NEWS: Dockable window "Find"

Makarius makarius at sketis.net
Wed Sep 25 19:48:31 CEST 2013


On Wed, 25 Sep 2013, Andrius Velykis wrote:

> Isabelle/Eclipse is not there because Eclipse is better or something. I 
> am not aiming at platform wars - Isabelle/Eclipse has been born out of 
> the fact that I like Eclipse and I wanted to build tools on top of 
> Eclipse and Isabelle. I do hope that people who also like Eclipse can 
> contribute or build upon Isabelle/Eclipse so that the project would 
> grow. Furthermore, I think that having different UIs on top of 
> Isabelle/Scala can help with better APIs and more general implementation 
> there.

These are very good reasons for Isabelle/Eclipse.  The PIDE document model 
of Isabelle/Scala was done in a way to support exactly that.  After some 
years working on the Isabelle/Scala basis and the Isabelle/jEdit front-end 
I had almost gotten the impression that nobody manages to pick up the 
challenge.  Maybe you have noticed the subtle changes in the wording of 
the "blurb" for Isabelle/jEdit:

   Isabelle2011-1 and Isabelle2012:

   Isabelle/jEdit is an example application within the PIDE
   framework --- it illustrates many of the ideas in a realistic
   manner, ready to be used right now in Isabelle applications.


   Isabelle2013:

   Isabelle/jEdit is the flagship application of the PIDE framework
   --- it is ready for small and large Isabelle applications, for
   beginners and experts alike.


   Isabelle2013-1:

   Isabelle/jEdit is the main example application of the PIDE
   framework and the default user-interface for Isabelle. It is targeted at
   beginners and experts alike.


So the slightly odd marketing talk about "flagship" has gone (I had 
copied that actually from PG Eclipse). Thanks to Isabelle/Eclipse the 
Isabelle/Scala/PIDE universe is populated by > 1 non-trivial applications.


> In the end, I am still playing catch-up with Isabelle/jEdit as well as 
> all the goodies in Eclipse (the JDT editor has some nifty features to 
> copy from). So props to Makarius for developing a nice PIDE and I hope 
> Isabelle/Eclipse will be as nice in the near future :)

I had a very productive summer this year, so there are many new things in 
the "main example application" of PIDE.

I am looking forward to see Isabelle/Eclipse catching up eventually (after 
you have finished your thesis).  It will help to make some general 
progress in the field, such that projects like 
https://itu.dk/research/tomeso/kopitiam/ won't have to go back again to 
the TTY loop, as is done there for Coq (even though the TTY speaks "XML" 
in Coq 8.4).


 	Makarius




More information about the isabelle-dev mailing list