--- a/Admin/build Sun Dec 28 14:40:43 2008 -0800
+++ b/Admin/build Sun Dec 28 14:41:47 2008 -0800
@@ -101,15 +101,6 @@
pushd "$ISABELLE_HOME/src/Pure" >/dev/null
"$ISABELLE_TOOL" make jar || fail "Failed to build Pure.jar!"
popd >/dev/null
-
- if [ -d "$HOME/lib/jedit/current" ]; then
- pushd "$ISABELLE_HOME/lib/jedit/plugin" >/dev/null
- ./mk
- [ -f ../isabelle.jar ] || fail "Failed to build jEdit plugin!"
- popd >/dev/null
- else
- echo "Warning: skipping jedit plugin"
- fi
}
--- a/src/Pure/General/markup.scala Sun Dec 28 14:40:43 2008 -0800
+++ b/src/Pure/General/markup.scala Sun Dec 28 14:41:47 2008 -0800
@@ -93,6 +93,10 @@
val CONTROL = "control"
val MALFORMED = "malformed"
+ val COMMAND_SPAN = "command_span"
+ val IGNORED_SPAN = "ignored_span"
+ val MALFORMED_SPAN = "malformed_span"
+
/* toplevel */