# HG changeset patch
# User wenzelm
# Date 1355483348 -3600
# Node ID 9605b0d93d1e5a1b71dd379f6adc228b50cbeb11
# Parent  33c92722cc3d9ef83a81fbd3c1c120e308c39acf
more formal class Command.Results;

diff -r 33c92722cc3d -r 9605b0d93d1e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -17,13 +17,30 @@
 {
   /** accumulated results from prover **/
 
-  type Results = SortedMap[Long, XML.Tree]
-  val empty_results: Results = SortedMap.empty
+  /* results */
+
+  object Results
+  {
+    val empty = new Results(SortedMap.empty)
+    def merge(rs: Iterable[Results]): Results = (empty /: rs.iterator)(_ ++ _)
+  }
+
+  final class Results private(private val rep: SortedMap[Long, XML.Tree])
+  {
+    def defined(serial: Long): Boolean = rep.isDefinedAt(serial)
+    def get(serial: Long): Option[XML.Tree] = rep.get(serial)
+    def entries: Iterator[(Long, XML.Tree)] = rep.iterator
+    def + (entry: (Long, XML.Tree)): Results = new Results(rep + entry)
+    def ++ (other: Results): Results = new Results(rep ++ other.rep)
+  }
+
+
+  /* state */
 
   sealed case class State(
     command: Command,
     status: List[Markup] = Nil,
-    results: Results = empty_results,
+    results: Results = Results.empty,
     markup: Markup_Tree = Markup_Tree.empty)
   {
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
@@ -93,7 +110,7 @@
   type Span = List[Token]
 
   def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span,
-    results: Results = empty_results, markup: Markup_Tree = Markup_Tree.empty): Command =
+    results: Results = Results.empty, markup: Markup_Tree = Markup_Tree.empty): Command =
   {
     val source: String =
       span match {
@@ -120,7 +137,7 @@
     Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), results, markup)
 
   def unparsed(source: String): Command =
-    unparsed(Document.no_id, source, empty_results, Markup_Tree.empty)
+    unparsed(Document.no_id, source, Results.empty, Markup_Tree.empty)
 
   def rich_text(id: Document.Command_ID, results: Results, body: XML.Body): Command =
   {
diff -r 33c92722cc3d -r 9605b0d93d1e src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -106,7 +106,7 @@
         val status = command_status(st.status)
         if (status.is_running) running += 1
         else if (status.is_finished) {
-          if (st.results.exists(p => is_warning(p._2))) warned += 1
+          if (st.results.entries.exists(p => is_warning(p._2))) warned += 1
           else finished += 1
         }
         else if (status.is_failed) failed += 1
diff -r 33c92722cc3d -r 9605b0d93d1e src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -65,7 +65,7 @@
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
           {
             val rendering = Rendering(snapshot, PIDE.options.value)
-            new Pretty_Tooltip(view, parent, rendering, x, y, Command.empty_results, body)
+            new Pretty_Tooltip(view, parent, rendering, x, y, Command.Results.empty, body)
             null
           }
         }
diff -r 33c92722cc3d -r 9605b0d93d1e src/Tools/jEdit/src/info_dockable.scala
--- a/src/Tools/jEdit/src/info_dockable.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/info_dockable.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -26,7 +26,7 @@
   /* implicit arguments -- owned by Swing thread */
 
   private var implicit_snapshot = Document.State.init.snapshot()
-  private var implicit_results = Command.empty_results
+  private var implicit_results = Command.Results.empty
   private var implicit_info: XML.Body = Nil
 
   private def set_implicit(snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
@@ -39,7 +39,7 @@
   }
 
   private def reset_implicit(): Unit =
-    set_implicit(Document.State.init.snapshot(), Command.empty_results, Nil)
+    set_implicit(Document.State.init.snapshot(), Command.Results.empty, Nil)
 
   def apply(view: View, snapshot: Document.Snapshot, results: Command.Results, info: XML.Body)
   {
diff -r 33c92722cc3d -r 9605b0d93d1e src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -62,7 +62,7 @@
   private var current_font_size: Int = 12
   private var current_body: XML.Body = Nil
   private var current_base_snapshot = Document.State.init.snapshot()
-  private var current_base_results = Command.empty_results
+  private var current_base_results = Command.Results.empty
   private var current_rendering: Rendering =
     Pretty_Text_Area.text_rendering(current_base_snapshot, current_base_results, Nil)._2
   private var future_rendering: Option[java.util.concurrent.Future[Unit]] = None
diff -r 33c92722cc3d -r 9605b0d93d1e src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Thu Dec 13 19:53:55 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Dec 14 12:09:08 2012 +0100
@@ -256,7 +256,7 @@
     snapshot.select_markup(range, Some(active_include), command_state =>
         {
           case Text.Info(info_range, elem @ Protocol.Dialog(_, serial, _))
-          if !command_state.results.isDefinedAt(serial) =>
+          if !command_state.results.defined(serial) =>
             Text.Info(snapshot.convert(info_range), elem)
           case Text.Info(info_range, elem @ XML.Elem(Markup(name, _), _))
           if name == Markup.GRAPHVIEW || name == Markup.SENDBACK =>
@@ -269,24 +269,25 @@
     val results =
       snapshot.select_markup[Command.Results](range, None, command_state =>
         { case _ => command_state.results }).map(_.info)
-    (Command.empty_results /: results)(_ ++ _)
+    (Command.Results.empty /: results)(_ ++ _)
   }
 
   def tooltip_message(range: Text.Range): XML.Body =
   {
     val msgs =
-      snapshot.cumulate_markup[Command.Results](range, Command.empty_results,
-        Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
-        {
-          case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
-          if name == Markup.WRITELN ||
-              name == Markup.WARNING ||
-              name == Markup.ERROR =>
-            msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
-          case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
-          if !body.isEmpty => msgs + (Document.new_id() -> msg)
-        }).toList.flatMap(_.info)
-    Pretty.separate(msgs.iterator.map(_._2).toList)
+      Command.Results.merge(
+        snapshot.cumulate_markup[Command.Results](range, Command.Results.empty,
+          Some(Set(Markup.WRITELN, Markup.WARNING, Markup.ERROR, Markup.BAD)), _ =>
+          {
+            case (msgs, Text.Info(_, XML.Elem(Markup(name, props @ Markup.Serial(serial)), body)))
+            if name == Markup.WRITELN ||
+                name == Markup.WARNING ||
+                name == Markup.ERROR =>
+              msgs + (serial -> XML.Elem(Markup(Markup.message(name), props), body))
+            case (msgs, Text.Info(_, msg @ XML.Elem(Markup(Markup.BAD, _), body)))
+            if !body.isEmpty => msgs + (Document.new_id() -> msg)
+          }).map(_.info))
+    Pretty.separate(msgs.entries.map(_._2).toList)
   }
 
 
@@ -420,7 +421,7 @@
 
   def output_messages(st: Command.State): List[XML.Tree] =
   {
-    st.results.iterator.map(_._2).filterNot(Protocol.is_result(_)).toList
+    st.results.entries.map(_._2).filterNot(Protocol.is_result(_)).toList
   }