# HG changeset patch
# User wenzelm
# Date 1281211792 -7200
# Node ID ed147003de4bc4eb7e4376e779156f68c296385d
# Parent  61d0fe8b96ac895fda3ee558dabef308893ec62f
simplified type XML.Tree: embed Markup directly, avoid slightly odd triple;
XML.cache_tree: actually store XML.Text as well;
added Isabelle_Process.Result.properties;

diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/General/markup.scala
--- a/src/Pure/General/markup.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/markup.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -214,3 +214,5 @@
 
   val DATA = "data"
 }
+
+sealed case class Markup(name: String, properties: List[(String, String)])
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/pretty.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -17,11 +17,11 @@
   object Block
   {
     def apply(indent: Int, body: List[XML.Tree]): XML.Tree =
-      XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent.toString)), body)
+      XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent.toString))), body)
 
     def unapply(tree: XML.Tree): Option[(Int, List[XML.Tree])] =
       tree match {
-        case XML.Elem(Markup.BLOCK, List((Markup.INDENT, indent)), body) =>
+        case XML.Elem(Markup(Markup.BLOCK, List((Markup.INDENT, indent))), body) =>
           Markup.parse_int(indent) match {
             case Some(i) => Some((i, body))
             case None => None
@@ -33,12 +33,12 @@
   object Break
   {
     def apply(width: Int): XML.Tree =
-      XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)),
+      XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width.toString))),
         List(XML.Text(Symbol.spaces(width))))
 
     def unapply(tree: XML.Tree): Option[Int] =
       tree match {
-        case XML.Elem(Markup.BREAK, List((Markup.WIDTH, width)), _) => Markup.parse_int(width)
+        case XML.Elem(Markup(Markup.BREAK, List((Markup.WIDTH, width))), _) => Markup.parse_int(width)
         case _ => None
       }
   }
@@ -50,7 +50,7 @@
 
   private def standard_format(tree: XML.Tree): List[XML.Tree] =
     tree match {
-      case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(standard_format)))
+      case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(standard_format)))
       case XML.Text(text) =>
         Library.separate(FBreak,
           Library.chunks(text).toList.map((s: CharSequence) => XML.Text(s.toString)))
@@ -82,7 +82,7 @@
 
     def content_length(tree: XML.Tree): Double =
       tree match {
-        case XML.Elem(_, _, body) => (0.0 /: body)(_ + content_length(_))
+        case XML.Elem(_, body) => (0.0 /: body)(_ + content_length(_))
         case XML.Text(s) => metric(s)
       }
 
@@ -122,10 +122,10 @@
           else format(ts, blockin, after, text.newline.blanks(blockin.toInt))
         case FBreak :: ts => format(ts, blockin, after, text.newline.blanks(blockin.toInt))
 
-        case XML.Elem(name, atts, body) :: ts =>
+        case XML.Elem(markup, body) :: ts =>
           val btext = format(body, blockin, breakdist(ts, after), text.copy(tx = Nil))
           val ts1 = if (text.nl < btext.nl) forcenext(ts) else ts
-          val btext1 = btext.copy(tx = XML.Elem(name, atts, btext.content) :: text.tx)
+          val btext1 = btext.copy(tx = XML.Elem(markup, btext.content) :: text.tx)
           format(ts1, blockin, after, btext1)
         case XML.Text(s) :: ts => format(ts, blockin, after, text.string(s, metric(s)))
       }
@@ -146,7 +146,7 @@
         case Block(_, body) => body.flatMap(fmt)
         case Break(wd) => List(XML.Text(Symbol.spaces(wd)))
         case FBreak => List(XML.Text(Symbol.space))
-        case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt)))
+        case XML.Elem(markup, body) => List(XML.Elem(markup, body.flatMap(fmt)))
         case XML.Text(_) => List(tree)
       }
     input.flatMap(standard_format).flatMap(fmt)
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/xml.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -24,11 +24,11 @@
       s.toString
     }
   }
-  case class Elem(name: String, attributes: Attributes, body: List[Tree]) extends Tree
+  case class Elem(markup: Markup, body: List[Tree]) extends Tree
   case class Text(content: String) extends Tree
 
-  def elem(name: String, body: List[Tree]) = Elem(name, Nil, body)
-  def elem(name: String) = Elem(name, Nil, Nil)
+  def elem(name: String, body: List[Tree]) = Elem(Markup(name, Nil), body)
+  def elem(name: String) = Elem(Markup(name, Nil), Nil)
 
 
   /* string representation */
@@ -56,9 +56,9 @@
 
   private def append_tree(tree: Tree, s: StringBuilder) {
     tree match {
-      case Elem(name, atts, Nil) =>
+      case Elem(Markup(name, atts), Nil) =>
         s ++= "<"; append_elem(name, atts, s); s ++= "/>"
-      case Elem(name, atts, ts) =>
+      case Elem(Markup(name, atts), ts) =>
         s ++= "<"; append_elem(name, atts, s); s ++= ">"
         for (t <- ts) append_tree(t, s)
         s ++= "</"; s ++= name; s ++= ">"
@@ -72,7 +72,7 @@
   private type State = Option[(String, List[Tree])]
 
   private def get_next(tree: Tree): State = tree match {
-    case Elem(_, _, body) => get_nexts(body)
+    case Elem(_, body) => get_nexts(body)
     case Text(content) => Some(content, Nil)
   }
   private def get_nexts(trees: List[Tree]): State = trees match {
@@ -127,14 +127,23 @@
           case Some(y) => y
           case None => store(x.map(p => (cache_string(p._1), cache_string(p._2))))
         }
+    def cache_markup(x: Markup): Markup =
+      lookup(x) match {
+        case Some(y) => y
+        case None =>
+          x match {
+            case Markup(name, props) =>
+              store(Markup(cache_string(name), cache_props(props)))
+          }
+      }
     def cache_tree(x: XML.Tree): XML.Tree =
       lookup(x) match {
         case Some(y) => y
         case None =>
           x match {
-            case XML.Elem(name, props, body) =>
-              store(XML.Elem(cache_string(name), cache_props(props), cache_trees(body)))
-            case XML.Text(text) => XML.Text(cache_string(text))
+            case XML.Elem(markup, body) =>
+              store(XML.Elem(cache_markup(markup), cache_trees(body)))
+            case XML.Text(text) => store(XML.Text(cache_string(text)))
           }
       }
     def cache_trees(x: List[XML.Tree]): List[XML.Tree] =
@@ -158,11 +167,11 @@
   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.DATA, Nil, List(data, t)) =>
+      case Elem(Markup(Markup.DATA, Nil), List(data, t)) =>
         val node = DOM(t)
         node.setUserData(Markup.DATA, data, null)
         node
-      case Elem(name, atts, ts) =>
+      case Elem(Markup(name, atts), ts) =>
         if (name == Markup.DATA)
           error("Malformed data element: " + tr.toString)
         val node = doc.createElement(name)
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/General/yxml.scala
--- a/src/Pure/General/yxml.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/General/yxml.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -64,7 +64,7 @@
     /* stack operations */
 
     def buffer(): ListBuffer[XML.Tree] = new ListBuffer[XML.Tree]
-    var stack: List[((String, XML.Attributes), ListBuffer[XML.Tree])] = List((("", Nil), buffer()))
+    var stack: List[(Markup, ListBuffer[XML.Tree])] = List((Markup("", Nil), buffer()))
 
     def add(x: XML.Tree)
     {
@@ -74,15 +74,16 @@
     def push(name: String, atts: XML.Attributes)
     {
       if (name == "") err_element()
-      else stack = ((name, atts), buffer()) :: stack
+      else stack = (Markup(name, atts), buffer()) :: stack
     }
 
     def pop()
     {
       (stack: @unchecked) match {
-        case ((("", _), _) :: _) => err_unbalanced("")
-        case (((name, atts), body) :: pending) =>
-          stack = pending; add(XML.Elem(name, atts, body.toList))
+        case ((Markup("", _), _) :: _) => err_unbalanced("")
+        case ((markup, body) :: pending) =>
+          stack = pending
+          add(XML.Elem(markup, body.toList))
       }
     }
 
@@ -100,8 +101,8 @@
       }
     }
     stack match {
-      case List((("", _), body)) => body.toList
-      case ((name, _), _) :: _ => err_unbalanced(name)
+      case List((Markup("", _), body)) => body.toList
+      case (Markup(name, _), _) :: _ => err_unbalanced(name)
     }
   }
 
@@ -116,7 +117,7 @@
   /* failsafe parsing */
 
   private def markup_failsafe(source: CharSequence) =
-    XML.Elem (Markup.MALFORMED, Nil,
+    XML.Elem (Markup(Markup.MALFORMED, Nil),
       List(XML.Text(source.toString.replace(X_string, "\\<^X>").replace(Y_string, "\\<^Y>"))))
 
   def parse_body_failsafe(source: CharSequence): List[XML.Tree] =
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/Isar/isar_document.scala
--- a/src/Pure/Isar/isar_document.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Isar/isar_document.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -14,7 +14,7 @@
   object Assign {
     def unapply(msg: XML.Tree): Option[List[XML.Tree]] =
       msg match {
-        case XML.Elem(Markup.ASSIGN, Nil, edits) => Some(edits)
+        case XML.Elem(Markup(Markup.ASSIGN, Nil), edits) => Some(edits)
         case _ => None
       }
   }
@@ -22,7 +22,7 @@
   object Edit {
     def unapply(msg: XML.Tree): Option[(Document.Command_ID, Document.State_ID)] =
       msg match {
-        case XML.Elem(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id)), Nil) =>
+        case XML.Elem(Markup(Markup.EDIT, List((Markup.ID, cmd_id), (Markup.STATE, state_id))), Nil) =>
           Some(cmd_id, state_id)
         case _ => None
       }
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Isar/keyword.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -55,7 +55,7 @@
   object Keyword_Decl {
     def unapply(msg: XML.Tree): Option[String] =
       msg match {
-        case XML.Elem(Markup.KEYWORD_DECL, List((Markup.NAME, name)), _) => Some(name)
+        case XML.Elem(Markup(Markup.KEYWORD_DECL, List((Markup.NAME, name))), _) => Some(name)
         case _ => None
       }
   }
@@ -63,7 +63,7 @@
   object Command_Decl {
     def unapply(msg: XML.Tree): Option[(String, String)] =
       msg match {
-        case XML.Elem(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind)), _) =>
+        case XML.Elem(Markup(Markup.COMMAND_DECL, List((Markup.NAME, name), (Markup.KIND, kind))), _) =>
           Some((name, kind))
         case _ => None
       }
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/PIDE/state.scala
--- a/src/Pure/PIDE/state.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -76,15 +76,15 @@
 
   def accumulate(message: XML.Tree): State =
     message match {
-      case XML.Elem(Markup.STATUS, _, elems) =>
+      case XML.Elem(Markup(Markup.STATUS, _), elems) =>
         (this /: elems)((state, elem) =>
           elem match {
-            case XML.Elem(Markup.UNPROCESSED, _, _) => state.set_status(Command.Status.UNPROCESSED)
-            case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
-            case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
-            case XML.Elem(Markup.FORKED, _, _) => state.add_forks(1)
-            case XML.Elem(Markup.JOINED, _, _) => state.add_forks(-1)
-            case XML.Elem(kind, atts, body) if Position.get_id(atts) == Some(command.id) =>
+            case XML.Elem(Markup(Markup.UNPROCESSED, _), _) => state.set_status(Command.Status.UNPROCESSED)
+            case XML.Elem(Markup(Markup.FINISHED, _), _) => state.set_status(Command.Status.FINISHED)
+            case XML.Elem(Markup(Markup.FAILED, _), _) => state.set_status(Command.Status.FAILED)
+            case XML.Elem(Markup(Markup.FORKED, _), _) => state.add_forks(1)
+            case XML.Elem(Markup(Markup.JOINED, _), _) => state.add_forks(-1)
+            case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
               atts match {
                 case Position.Range(begin, end) =>
                   if (kind == Markup.ML_TYPING) {
@@ -94,7 +94,7 @@
                   }
                   else if (kind == Markup.ML_REF) {
                     body match {
-                      case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+                      case List(XML.Elem(Markup(Markup.ML_DEF, atts), _)) =>
                         state.add_markup(command.markup_node(
                           begin - 1, end - 1,
                           Command.RefInfo(
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/System/isabelle_process.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -45,26 +45,26 @@
 
   class Result(val message: XML.Elem)
   {
-    def kind = message.name
+    def kind = message.markup.name
+    def properties = message.markup.properties
     def body = message.body
 
     def is_raw = Kind.is_raw(kind)
     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.READY, Nil, Nil))
+    def is_ready = is_status && body == List(XML.Elem(Markup(Markup.READY, Nil), Nil))
 
     override def toString: String =
     {
       val res =
         if (is_status) message.body.map(_.toString).mkString
         else Pretty.string_of(message.body)
-      val props = message.attributes
-      if (props.isEmpty)
+      if (properties.isEmpty)
         kind.toString + " [[" + res + "]]"
       else
         kind.toString + " " +
-          (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
+          (for ((x, y) <- properties) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
     }
 
     def cache(c: XML.Cache): Result = new Result(c.cache_tree(message).asInstanceOf[XML.Elem])
@@ -98,7 +98,7 @@
     if (kind == Markup.INIT) {
       for ((Markup.PID, p) <- props) pid = p
     }
-    receiver ! new Result(XML.Elem(kind, props, body))
+    receiver ! new Result(XML.Elem(Markup(kind, props), body))
   }
 
   private def put_result(kind: String, text: String)
@@ -300,7 +300,7 @@
             val header = read_chunk()
             val body = read_chunk()
             header match {
-              case List(XML.Elem(name, props, Nil))
+              case List(XML.Elem(Markup(name, props), Nil))
                   if name.size == 1 && Kind.markup.isDefinedAt(name(0)) =>
                 put_result(Kind.markup(name(0)), props, body)
               case _ => throw new Protocol_Error("bad header: " + header.toString)
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/System/session.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -138,7 +138,7 @@
     {
       raw_results.event(result)
 
-      val target_id: Option[Session.Entity_ID] = Position.get_id(result.message.attributes)
+      val target_id: Option[Session.Entity_ID] = Position.get_id(result.properties)
       val target: Option[Session.Entity] =
         target_id match {
           case None => None
diff -r 61d0fe8b96ac -r ed147003de4b src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Pure/Thy/html.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -42,7 +42,7 @@
   // document markup
 
   def span(cls: String, body: List[XML.Tree]): XML.Elem =
-    XML.Elem(SPAN, List((CLASS, cls)), body)
+    XML.Elem(Markup(SPAN, List((CLASS, cls))), body)
 
   def hidden(txt: String): XML.Elem =
     span(Markup.HIDDEN, List(XML.Text(txt)))
@@ -52,7 +52,7 @@
 
   def spans(tree: XML.Tree): List[XML.Tree] =
     tree match {
-      case XML.Elem(name, _, ts) =>
+      case XML.Elem(Markup(name, _), ts) =>
         List(XML.elem(Markup.DATA, List(tree, span(name, ts.flatMap(spans)))))
       case XML.Text(txt) =>
         val ts = new ListBuffer[XML.Tree]
diff -r 61d0fe8b96ac -r ed147003de4b src/Tools/jEdit/src/jedit/output_dockable.scala
--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 21:22:39 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sat Aug 07 22:09:52 2010 +0200
@@ -68,8 +68,8 @@
               val snapshot = doc_view.model.snapshot()
               val filtered_results =
                 snapshot.document.current_state(cmd).results filter {
-                  case XML.Elem(Markup.TRACING, _, _) => show_tracing
-                  case XML.Elem(Markup.DEBUG, _, _) => show_debug
+                  case XML.Elem(Markup(Markup.TRACING, _), _) => show_tracing
+                  case XML.Elem(Markup(Markup.DEBUG, _), _) => show_debug
                   case _ => true
                 }
               html_panel.render(filtered_results)