# HG changeset patch
# User haftmann
# Date 1315341452 -7200
# Node ID 72d322c2786f57a6b261c373f4dae6d9f6742367
# Parent  19e1c6e922b60473a5703ccc20595f13b6c45cc2# Parent  ff6b9eb9c5ef66c760fa5f36f064100924c6b99a
merged

diff -r ff6b9eb9c5ef -r 72d322c2786f NEWS
--- a/NEWS	Tue Sep 06 22:04:14 2011 +0200
+++ b/NEWS	Tue Sep 06 22:37:32 2011 +0200
@@ -6,6 +6,30 @@
 
 *** General ***
 
+* Improved Isabelle/jEdit Prover IDE (PIDE), which can be invoked as
+"isabelle jedit" on the command line.
+
+  . Management of multiple theory files directly from the editor
+    buffer store -- bypassing the file-system (no requirement to save
+    files for checking).
+
+  . Markup of formal entities within the text buffer, with semantic
+    highlighting, tooltips and hyperlinks to jump to defining source
+    positions.
+
+  . Refined scheduling of proof checking and printing of results,
+    based on interactive editor view.  (Note: jEdit folding and
+    narrowing allows to restrict buffer perspectives explicitly.)
+
+  . Reduced CPU performance requirements, usable on machines with few
+    cores.
+
+  . Reduced memory requirements due to pruning of unused document
+    versions (garbage collection).
+
+See also ~~/src/Tools/jEdit/README.html for further information,
+including some remaining limitations.
+
 * Theory loader: source files are identified by content via SHA1
 digests.  Discontinued former path/modtime identification and optional
 ISABELLE_FILE_IDENT plugin scripts.
diff -r ff6b9eb9c5ef -r 72d322c2786f src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html	Tue Sep 06 22:04:14 2011 +0200
+++ b/src/Tools/jEdit/README.html	Tue Sep 06 22:37:32 2011 +0200
@@ -139,6 +139,11 @@
   to a theory ("<b>uses</b>").<br/>
   <em>Workaround:</em> Re-use files manually within the prover.</li>
 
+  <li>Crude management of new Isar commands that are defined within
+  the running session.<br/>
+  <em>Workaround:</em> Force re-parsing of files using such commands
+  via reload menu of jEdit.</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>