# HG changeset patch
# User wenzelm
# Date 1321017878 -3600
# Node ID 4f974c0c5c2fb0b9bcd29c287f5d56c52ccfe265
# Parent  388fb71623dda4bf3d1c30e86d881955853f760b
prefer statically typed Text.Markup;

diff -r 388fb71623dd -r 4f974c0c5c2f src/Pure/PIDE/blob.scala
--- a/src/Pure/PIDE/blob.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Pure/PIDE/blob.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -11,7 +11,7 @@
 {
   sealed case class State(val blob: Blob, val markup: Markup_Tree = Markup_Tree.empty)
   {
-    def + (info: Text.Info[Any]): State = copy(markup = markup + info)
+    def + (info: Text.Markup): State = copy(markup = markup + info)
   }
 }
 
diff -r 388fb71623dd -r 4f974c0c5c2f src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -25,12 +25,12 @@
     /* content */
 
     def add_status(st: Markup): State = copy(status = st :: status)
-    def add_markup(info: Text.Info[Any]): State = copy(markup = markup + info)
+    def add_markup(m: Text.Markup): State = copy(markup = markup + m)
     def add_result(serial: Long, result: XML.Tree): State =
       copy(results = results + (serial -> result))
 
-    def root_info: Text.Info[Any] =
-      new Text.Info(command.range,
+    def root_info: Text.Markup =
+      Text.Info(command.range,
         XML.Elem(Markup(Markup.STATUS, Nil), status.reverse.map(XML.Elem(_, Nil))))
     def root_markup: Markup_Tree = markup + root_info
 
@@ -53,7 +53,7 @@
               if id == command.id && command.range.contains(command.decode(raw_range)) =>
                 val range = command.decode(raw_range)
                 val props = Position.purge(atts)
-                val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
+                val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
               case _ =>
                 // FIXME System.err.println("Ignored report message: " + msg)
diff -r 388fb71623dd -r 4f974c0c5c2f src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Pure/PIDE/markup_tree.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -19,7 +19,7 @@
 
   object Branches
   {
-    type Entry = (Text.Info[Any], Markup_Tree)
+    type Entry = (Text.Markup, Markup_Tree)
     type T = SortedMap[Text.Range, Entry]
 
     val empty = SortedMap.empty[Text.Range, Entry](Text.Range.Ordering)
@@ -41,7 +41,7 @@
 
   val empty = new Markup_Tree(Branches.empty)
 
-  type Select[A] = PartialFunction[Text.Info[Any], A]
+  type Select[A] = PartialFunction[Text.Markup, A]
 }
 
 
@@ -55,7 +55,7 @@
       case list => list.mkString("Tree(", ",", ")")
     }
 
-  def + (new_info: Text.Info[Any]): Markup_Tree =
+  def + (new_info: Text.Markup): Markup_Tree =
   {
     val new_range = new_info.range
     branches.get(new_range) match {
@@ -126,7 +126,7 @@
   }
 
   def swing_tree(parent: DefaultMutableTreeNode)
-    (swing_node: Text.Info[Any] => DefaultMutableTreeNode)
+    (swing_node: Text.Markup => DefaultMutableTreeNode)
   {
     for ((_, (info, subtree)) <- branches) {
       val current = swing_node(info)
diff -r 388fb71623dd -r 4f974c0c5c2f src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Pure/PIDE/text.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -115,6 +115,8 @@
       catch { case ERROR(_) => None }
   }
 
+  type Markup = Info[XML.Tree]
+
 
   /* editing */
 
diff -r 388fb71623dd -r 4f974c0c5c2f src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 11 14:07:20 2011 +0100
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Fri Nov 11 14:24:38 2011 +0100
@@ -152,7 +152,7 @@
     val root = data.root
     val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for ((command, command_start) <- snapshot.node.command_range() if !stopped) {
-      snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Info[Any]) =>
+      snapshot.command_state(command).root_markup.swing_tree(root)((info: Text.Markup) =>
           {
             val range = info.range + command_start
             val content = command.source(info.range).replace('\n', ' ')