# HG changeset patch
# User huffman
# Date 1230504107 28800
# Node ID ff41885a12346968d25fb38d9ebea7725eea979c
# Parent  7b09385234f9315c936860df5477908c8854476d# Parent  3d25e96ceb9812da209a8cd61b89f106fe009c24
merged

diff -r 7b09385234f9 -r ff41885a1234 Admin/build
--- 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
 }
 
 
diff -r 7b09385234f9 -r ff41885a1234 src/Pure/General/markup.scala
--- 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 */