--- 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)
--- /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
--- 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.
--- 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,<MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>\n\n,;