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