--- a/src/Tools/jEdit/README Sun Sep 04 15:49:59 2011 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,62 +0,0 @@
-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
-
-
-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.
-
-- ToggleButton selected state is not rendered if window focus is lost,
- which is probably a genuine feature of the Apple look-and-feel.
-
-- 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.
-
-- Missing glyphs are collected from other fonts (like Emacs, Firefox).
- This is actually an advantage over the Oracle/Sun JVM on Windows or
- Linux, but probably also the deeper reason for the other oddities of
- Apple font management.
-
-- The native font renderer of -Dapple.awt.graphics.UseQuartz=true
- fails to handle the infinitesimal font size of "hidden" text (e.g.
- used in Isabelle sub/superscripts).
-
-
-Known problems with OpenJDK
-===========================
-
-- The 2D rendering engine of OpenJDK 1.6.x distorts the appearance of
- the jEdit text area. Always use official JRE 1.6.x from
- Sun/Oracle/Apple.
-
-
-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/
--- a/src/Tools/jEdit/README.html Sun Sep 04 15:49:59 2011 +0200
+++ b/src/Tools/jEdit/README.html Sun Sep 04 16:37:22 2011 +0200
@@ -12,7 +12,12 @@
<body>
-<h2>The Isabelle/jEdit Prover IDE</h2>
+<h2>The Isabelle/jEdit Prover IDE (based on Isabelle/Scala)</h2>
+
+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.
<ul>
@@ -116,30 +121,23 @@
</ul>
-<h2>Limitations and workrounds (January 2011)</h2>
+<h2>Limitations and workrounds (September 2011)</h2>
<ul>
<li>No way to start/stop prover or switch to a different logic.<br/>
<em>Workaround:</em> Change options and restart editor.</li>
- <li>Limited support for dependencies between multiple theory buffers.<br/>
- <em>Workaround:</em> Load required files manually.</li>
-
- <li>No reclaiming of old/unused document versions in prover or
- editor.<br/>
- <em>Workaround:</em> Avoid large files; restart after a few hours of use.</li>
-
<li>Incremental reparsing sometimes produces unexpected command
spans.<br/>
<em>Workaround:</em> Cut/paste larger parts or reload buffer.</li>
- <li>Command execution sometimes gets stuck (purple background).<br/>
- <em>Workaround:</em> Force reparsing as above.</li>
+ <li>Odd behavior of some diagnostic commands, notably those starting
+ external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
+ <em>Workaround:</em> Avoid such commands.</li>
- <li>Odd behavior of some diagnostic commands, notably those
- starting external processes asynchronously
- (e.g. <tt>thy_deps</tt>, <tt>sledgehammer</tt>).<br/>
- <em>Workaround:</em> Avoid such commands.</li>
+ <li>Lack of dependency managed for auxiliary files that contribute
+ to a theory ("<b>uses</b>").<br/>
+ <em>Workaround:</em> Re-use files manually within the prover.</li>
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
@@ -149,6 +147,59 @@
General.</li>
</ul>
+
+<h2>Known problems with Mac OS</h2>
+
+<ul>
+
+<li>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.</li>
+
+<li>ToggleButton selected state is not rendered if window focus is
+ lost, which is probably a genuine feature of the Apple
+ look-and-feel.</li>
+
+<li>Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold. IsabelleText font files need to be installed/updated
+ manually.</li>
+
+<li>Missing glyphs are collected from other fonts (like Emacs,
+ Firefox). This is actually an advantage over the Oracle/Sun JVM on
+ Windows or Linux, but probably also the deeper reason for the other
+ oddities of Apple font management.</li>
+
+<li>The native font renderer of -Dapple.awt.graphics.UseQuartz=true
+ (not enabled by default) fails to handle the infinitesimal font size
+ of "hidden" text (e.g. used in Isabelle sub/superscripts).</li>
+
+</ul>
+
+
+<h2>Known problems with OpenJDK 1.6.x</h2>
+
+<ul>
+
+<li>The 2D rendering engine of OpenJDK 1.6.x distorts the appearance
+ of the jEdit text area. Always use official JRE 1.6.x from
+ Sun/Oracle/Apple.</li>
+
+<li>jEdit on OpenJDK is generally not supported.</li>
+
+</ul>
+
+
+<h2>Licenses and home sites of contributing systems</h2>
+
+<ul>
+
+<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
+
+<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org/</li>
+
+<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org/</li>
+
+</ul>
+
</body>
</html>
-
--- a/src/Tools/jEdit/README_BUILD Sun Sep 04 15:49:59 2011 +0200
+++ b/src/Tools/jEdit/README_BUILD Sun Sep 04 16:37:22 2011 +0200
@@ -1,14 +1,14 @@
Requirements for instantaneous build from sources
=================================================
-* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_26
- http://java.sun.com/javase/downloads/index.jsp
+* Official Java JDK from Sun/Oracle/Apple, e.g. 1.6.0_27
+ http://www.oracle.com/technetwork/java/javase/downloads/index.html
* Scala Compiler 2.8.1.final
http://www.scala-lang.org
* Auxiliary jedit_build component
- http://www4.in.tum.de/~wenzelm/test/jedit_build-20110521.tar.gz
+ http://www4.in.tum.de/~wenzelm/test/jedit_build-20110622.tar.gz
Important settings within Isabelle environment