# HG changeset patch
# User wenzelm
# Date 1281213837 -7200
# Node ID 968844caaff9e55a910f9c50eb94535617aa1aea
# Parent  ed147003de4bc4eb7e4376e779156f68c296385d
simplified some Markup;

diff -r ed147003de4b -r 968844caaff9 src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -183,7 +183,7 @@
 
   /* interactive documents */
 
-  val ASSIGN = "assign"
+  val Assign = Markup("assign", Nil)
   val EDIT = "edit"
 
 
@@ -207,12 +207,12 @@
   val SIGNAL = "signal"
   val EXIT = "exit"
 
-  val READY = "ready"
+  val Ready = Markup("ready", Nil)
 
 
   /* system data */
 
-  val DATA = "data"
+  val Data = Markup("data", Nil)
 }
 
 sealed case class Markup(name: String, properties: List[(String, String)])
diff -r ed147003de4b -r 968844caaff9 src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -159,7 +159,7 @@
   /* document object model (W3C DOM) */
 
   def get_data(node: org.w3c.dom.Node): Option[XML.Tree] =
-    node.getUserData(Markup.DATA) match {
+    node.getUserData(Markup.Data.name) match {
       case tree: XML.Tree => Some(tree)
       case _ => None
     }
@@ -167,12 +167,12 @@
   def document_node(doc: org.w3c.dom.Document, tree: Tree): org.w3c.dom.Node =
   {
     def DOM(tr: Tree): org.w3c.dom.Node = tr match {
-      case Elem(Markup(Markup.DATA, Nil), List(data, t)) =>
+      case Elem(Markup.Data, List(data, t)) =>
         val node = DOM(t)
-        node.setUserData(Markup.DATA, data, null)
+        node.setUserData(Markup.Data.name, data, null)
         node
       case Elem(Markup(name, atts), ts) =>
-        if (name == Markup.DATA)
+        if (name == Markup.Data.name)
           error("Malformed data element: " + tr.toString)
         val node = doc.createElement(name)
         for ((name, value) <- atts) node.setAttribute(name, value)
diff -r ed147003de4b -r 968844caaff9 src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -117,7 +117,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup(Markup.MALFORMED, Nil),
+    XML.elem (Markup.MALFORMED,
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
diff -r ed147003de4b -r 968844caaff9 src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -14,7 +14,7 @@
   object Assign {
     def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
       msg match {
-        case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits)
+        case XML.Elem(Markup.Assign, edits) => Some(edits)
         case _ => None
       }
   }
diff -r ed147003de4b -r 968844caaff9 src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -53,7 +53,7 @@
     def is_control = Kind.is_control(kind)
     def is_system = Kind.is_system(kind)
     def is_status = kind == Markup.STATUS
-    def is_ready = is_status && body == List(XML.Elem(Markup(Markup.READY, Nil), Nil))
+    def is_ready = is_status && body == List(XML.Elem(Markup.Ready, Nil))
 
     override def toString: String =
     {
diff -r ed147003de4b -r 968844caaff9 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Aug 07 22:09:52 2010 +0200
+++ b/src/Pure/Thy/html.scala	Sat Aug 07 22:43:57 2010 +0200
@@ -53,7 +53,7 @@
   def spans(tree: XML.Tree): List[XML.Tree] =
     tree match {
       case XML.Elem(Markup(name, _), ts) =>
-        List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
+        List(XML.Elem(Markup.Data, List(tree, span(name, ts.flatMap(spans)))))
       case XML.Text(txt) =>
         val ts = new ListBuffer[XML.Tree]
         val t = new StringBuilder