# HG changeset patch # User wenzelm # Date 1275336520 -7200 # Node ID ffd587207d5d6211d2d38ee4eed2d7e9a0e347a8 # Parent b2769ba027b03d0e6e8f520ed0c8fcdc6c5b2170 notes on Isabelle/jEdit; diff -r b2769ba027b0 -r ffd587207d5d NEWS --- a/NEWS Mon May 31 21:29:27 2010 +0200 +++ b/NEWS Mon May 31 22:08:40 2010 +0200 @@ -591,6 +591,11 @@ ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}" +* The preliminary Isabelle/jEdit application demonstrates the emerging +Isabelle/Scala layer for advanced prover interaction and integration. +See src/Tools/jEdit or "isabelle jedit" provided by the properly built +component. + New in Isabelle2009-1 (December 2009) diff -r b2769ba027b0 -r ffd587207d5d src/Tools/jEdit/README --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/README Mon May 31 22:08:40 2010 +0200 @@ -0,0 +1,77 @@ +Isabelle/jEdit based on Isabelle/Scala +====================================== + +The Isabelle/Scala layer that is already part of Isabelle/Pure +provides some general infrastructure for advanced prover interaction +and integration. The Isabelle/jEdit application serves as an example +for asynchronous proof checking with support for parallel processing. + +See also the paper: + + Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala + and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors, + User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite + Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS. + http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf + + +Some limitations of the current implementation (as of Isabelle2009-2): + + * No provisions for editing multiple theory files. + + * No reclaiming of old/unused document versions. Memory will fill + up eventually, both on the JVM and ML side. + + * No support for non-local markup, e.g. commands reporting on + previous commands (proof end on proof head), or markup produced by + loading external files. + + * Some performance bottlenecks for massive amount of markup, + e.g. when processing large ML sections. + + * General lack of various conveniences known from Proof General. + +Despite these shortcomings, Isabelle/jEdit already demonstrates that +interactive theorem proving can be much more than command-line +interaction via TTY or editor front-ends (such as Proof General and +its many remakes). + + +Known problems with Mac OS +========================== + +- The MacOSX plugin for jEdit disrupts regular C-X/C/V operations, + e.g. between the editor and the Console plugin, which is a standard + swing text box. Similar for search boxes etc. + +- Anti-aliasing does not really work as well as for Linux or Windows. + (General Apple/Swing problem?) + +- Font.createFont mangles the font family of non-regular fonts, + e.g. bold. IsabelleText font files need to be installed manually. + +- ToggleButton selected state is not rendered if window focus is lost, + which is probably a genuine feature of the Apple look-and-feel. + + +Windows/Linux +============= + +- Works best with Sun Java 1.6.x -- avoid OpenJDK for now. + + +Licenses and home sites of contributing systems +=============================================== + +* Scala: BSD-style + http://www.scala-lang.org + +* jEdit: GPL (with special cases) + http://www.jedit.org/ + +* Lobo/Cobra: GPL and LGPL + http://lobobrowser.org/ + + + Makarius + 31-May-2010 diff -r b2769ba027b0 -r ffd587207d5d src/Tools/jEdit/README_BUILD --- a/src/Tools/jEdit/README_BUILD Mon May 31 21:29:27 2010 +0200 +++ b/src/Tools/jEdit/README_BUILD Mon May 31 22:08:40 2010 +0200 @@ -2,7 +2,7 @@ Requirements to build from sources ================================== -* Proper Java JRE/JDK from Sun, e.g. 1.6.0_18 +* Proper Java JRE/JDK from Sun, e.g. 1.6.0_20 http://java.sun.com/javase/downloads/index.jsp * Netbeans 6.8 @@ -13,7 +13,7 @@ http://sourceforge.net/projects/erlybird/files/nb-scala/6.8v1.1.0rc2 http://blogtrader.net/dcaoyuan/category/NetBeans -* jEdit 4.3.1 or 4.3.2 +* jEdit 4.3.2 http://www.jedit.org/ Netbeans Project "jEdit": install official sources as ./contrib/jEdit/. @@ -31,7 +31,8 @@ * Isabelle/Pure Scala components Netbeans Library "Isabelle-Pure" = ~~/lib/classes/Pure.jar -* Scala Compiler +* Scala Compiler 2.8 + http://www.scala-lang.org Netbeans Library "Scala-compiler" = $SCALA_HOME/lib/scala-compiler.jar @@ -74,20 +75,3 @@ releases. (See http://java.sun.com/j2se/1.5.0/docs/guide/jpda/conninv.html) ----------------------------------------------------------------------- - - -Known problems with Mac OS -========================== - -- The MacOSX plugin disrupts regular C-X/C/V operations, e.g. between - the editor and the Console plugin, which is a standard swing text - box. Similar for search boxes etc. - -- Anti-aliasing does not really work as well as for Linux or Windows. - (General Apple/Swing problem?) - -- Font.createFont mangles the font family of non-regular fonts, - e.g. bold. - -- ToggleButton selected state is not rendered if window focus is lost, - which is probably a genuine feature of the Apple look-and-feel. diff -r b2769ba027b0 -r ffd587207d5d src/Tools/jEdit/makedist --- a/src/Tools/jEdit/makedist Mon May 31 21:29:27 2010 +0200 +++ b/src/Tools/jEdit/makedist Mon May 31 22:08:40 2010 +0200 @@ -84,6 +84,7 @@ cp -R jars/. "$JEDIT/jars/." cp -R "$THIS/dist-template/." "$JEDIT/." +cp "$THIS/README" "$JEDIT/." perl -i -e 'while (<>) { if (m/NAME="javacc"/) { print qq,\n\n,;