# HG changeset patch
# User wenzelm
# Date 1294938013 -3600
# Node ID d060ccad02bd31f8a1d5d29eea4d00ab34655465
# Parent  3837045cc8a182974593eb245435c413112f0573
updated Isabelle/jEdit limitations and workarounds;

diff -r 3837045cc8a1 -r d060ccad02bd src/Tools/jEdit/README
--- a/src/Tools/jEdit/README	Thu Jan 13 17:39:35 2011 +0100
+++ b/src/Tools/jEdit/README	Thu Jan 13 18:00:13 2011 +0100
@@ -15,25 +15,6 @@
   http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
 
 
-Some limitations of the current implementation:
-
-  * No provisions for theory file dependencies inside the editor.
-
-  * 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.
-
-  * 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
 ==========================
 
diff -r 3837045cc8a1 -r d060ccad02bd src/Tools/jEdit/dist-template/README.html
--- a/src/Tools/jEdit/dist-template/README.html	Thu Jan 13 17:39:35 2011 +0100
+++ b/src/Tools/jEdit/dist-template/README.html	Thu Jan 13 18:00:13 2011 +0100
@@ -34,6 +34,40 @@
 
 </ul>
 
+<h2>Limitations and workrounds (January 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>Multiple theory buffers cannot depend on each other, imports are
+  resolved via the file-system.<br/>
+  <em>Workaround:</em> Save/reload 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>, <tt>sledgehammer</tt>).<br/>
+  <em>Workaround:</em> Avoid such commands.</li>
+
+  <li>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.</li>
+
+  <li>General lack of various conveniences known from Proof
+  General.</li>
+</ul>
+
 </body>
 </html>