src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Thu Dec 13 13:52:18 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Dec 13 17:29:23 2012 +0100
@@ -17,11 +17,14 @@
 {
   /** accumulated results from prover **/
 
+  type Results = SortedMap[Long, XML.Tree]
+  val empty_results: Results = SortedMap.empty
+
   sealed case class State(
-    val command: Command,
-    val status: List[Markup] = Nil,
-    val results: SortedMap[Long, XML.Tree] = SortedMap.empty,
-    val markup: Markup_Tree = Markup_Tree.empty)
+    command: Command,
+    status: List[Markup] = Nil,
+    results: Results = empty_results,
+    markup: Markup_Tree = Markup_Tree.empty)
   {
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
       markup.to_XML(command.range, command.source, filter)
@@ -89,8 +92,8 @@
 
   type Span = List[Token]
 
-  def apply(id: Document.Command_ID, node_name: Document.Node.Name,
-    span: Span, markup: Markup_Tree): Command =
+  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
+    results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {
@@ -107,21 +110,23 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source, markup)
+    new Command(id, node_name, span1.toList, source, results, markup)
   }
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
 
-  def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
-    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
+  def unparsed(id: Document.Command_ID, source: String, results: Results, markup: Markup_Tree)
+      : Command =
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
 
-  def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
+  def unparsed(source: String): Command =
+    unparsed(Document.no_id, source, empty_results, Markup_Tree.empty)
 
-  def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+  def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
   {
     val text = XML.content(body)
     val markup = Markup_Tree.from_XML(body)
-    unparsed(id, text, markup)
+    unparsed(id, text, results, markup)
   }
 
 
@@ -152,6 +157,7 @@
     val node_name: Document.Node.Name,
     val span: Command.Span,
     val source: String,
+    val init_results: Command.Results,
     val init_markup: Markup_Tree)
 {
   /* classification */
@@ -188,5 +194,6 @@
 
   /* accumulated results */
 
-  val init_state: Command.State = Command.State(this, markup = init_markup)
+  val init_state: Command.State =
+    Command.State(this, results = init_results, markup = init_markup)
 }