# HG changeset patch
# User wenzelm
# Date 1331849182 -3600
# Node ID 9ff441f295c23ee015a158783f016699f10daee6
# Parent  7bd0780c0bd3d3a97e03b78e880d36cc9cc98019
Isabelle/jEdit supports user-defined Isar commands within the running session;

diff -r 7bd0780c0bd3 -r 9ff441f295c2 NEWS
--- a/NEWS	Thu Mar 15 22:21:28 2012 +0100
+++ b/NEWS	Thu Mar 15 23:06:22 2012 +0100
@@ -10,6 +10,7 @@
 
   - markup for bound variables
   - markup for types of term variables (e.g. displayed as tooltips)
+  - support for user-defined Isar commands within the running session
 
 * Updated and extended reference manuals ("isar-ref" and
 "implementation"); reduced remaining material in old "ref" manual.
@@ -371,6 +372,9 @@
 
 *** ML ***
 
+* Outer syntax keywords for user-defined Isar commands need to be
+defined explicitly in the theory header.  Minor INCOMPATIBILITY.
+
 * Antiquotation @{keyword "name"} produces a parser for outer syntax
 from a minor keyword introduced via theory header declaration.
 
diff -r 7bd0780c0bd3 -r 9ff441f295c2 src/Tools/jEdit/README.html
--- a/src/Tools/jEdit/README.html	Thu Mar 15 22:21:28 2012 +0100
+++ b/src/Tools/jEdit/README.html	Thu Mar 15 23:06:22 2012 +0100
@@ -156,7 +156,7 @@
 </ul>
 
 
-<h2>Limitations and workrounds (October 2011)</h2>
+<h2>Limitations and workrounds (March 2012)</h2>
 
 <ul>
   <li>No way to start/stop prover or switch to a different logic.<br/>
@@ -174,11 +174,6 @@
   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 way to delete document nodes from the overall collection of
   theories.<br/>
   <em>Workaround:</em> Restart whole Isabelle/jEdit session in