# HG changeset patch
# User wenzelm
# Date 1315147042 -7200
# Node ID f4b42f310f86c0d28f8a99a678effb998796faea
# Parent 5199ee17c7d73895240611eea18fe4bde73a9619
updated READMEs;
diff -r 5199ee17c7d7 -r f4b42f310f86 src/Tools/jEdit/README
--- 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/
diff -r 5199ee17c7d7 -r f4b42f310f86 src/Tools/jEdit/README.html
--- 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 @@
-The Isabelle/jEdit Prover IDE
+The Isabelle/jEdit Prover IDE (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.
-Limitations and workrounds (January 2011)
+Limitations and workrounds (September 2011)
- No way to start/stop prover or switch to a different logic.
Workaround: Change options and restart editor.
- - Limited support for dependencies between multiple theory buffers.
- Workaround: Load required files manually.
-
- - No reclaiming of old/unused document versions in prover or
- editor.
- Workaround: Avoid large files; restart after a few hours of use.
-
- Incremental reparsing sometimes produces unexpected command
spans.
Workaround: Cut/paste larger parts or reload buffer.
- - Command execution sometimes gets stuck (purple background).
- Workaround: Force reparsing as above.
+ - Odd behavior of some diagnostic commands, notably those starting
+ external processes asynchronously (e.g. thy_deps).
+ Workaround: Avoid such commands.
- - Odd behavior of some diagnostic commands, notably those
- starting external processes asynchronously
- (e.g. thy_deps, sledgehammer).
- Workaround: Avoid such commands.
+ - Lack of dependency managed for auxiliary files that contribute
+ to a theory ("uses").
+ Workaround: Re-use files manually within the prover.
- 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.
+
+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.
+
+- Font.createFont mangles the font family of non-regular fonts,
+ e.g. bold. IsabelleText font files need to be installed/updated
+ 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
+ (not enabled by default) fails to handle the infinitesimal font size
+ of "hidden" text (e.g. used in Isabelle sub/superscripts).
+
+
+
+
+Known problems with OpenJDK 1.6.x
+
+
+
+- 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.
+
+- jEdit on OpenJDK is generally not supported.
+
+
+
+
+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/
+
+
+