# HG changeset patch
# User wenzelm
# Date 1230492339 -3600
# Node ID 26fcfca1db9df242f621aa874a5cccd74917d3da
# Parent  85889d58b5da55af6c6e70c16968ff030687eb58
more markup elements;

diff -r 85889d58b5da -r 26fcfca1db9d src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sun Dec 28 16:39:27 2008 +0100
+++ b/src/Pure/General/markup.scala	Sun Dec 28 20:25:39 2008 +0100
@@ -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 */