--- 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
==========================
--- 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>