# HG changeset patch
# User wenzelm
# Date 1396376545 -7200
# Node ID a6f8c3566560fd9e8955c7240f4ac19cdc9e037d
# Parent  ecbdfe30bf7f625d0b63ec1d1e0349cc1f8860d0
more direct command states -- merge_results is hardly ever needed;

diff -r ecbdfe30bf7f -r a6f8c3566560 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Apr 01 17:29:47 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Apr 01 20:22:25 2014 +0200
@@ -434,13 +434,13 @@
       range: Text.Range,
       info: A,
       elements: Elements,
-      result: Command.Results => (A, Text.Markup) => Option[A],
+      result: List[Command.State] => (A, Text.Markup) => Option[A],
       status: Boolean = false): List[Text.Info[A]]
 
     def select[A](
       range: Text.Range,
       elements: Elements,
-      result: Command.Results => Text.Markup => Option[A],
+      result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
   }
 
@@ -729,7 +729,7 @@
           range: Text.Range,
           info: A,
           elements: Elements,
-          result: Command.Results => (A, Text.Markup) => Option[A],
+          result: List[Command.State] => (A, Text.Markup) => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
           val former_range = revert(range)
@@ -743,7 +743,7 @@
             (command, command_start) <- command_range_iterator
             chunk <- command.chunks.get(file_name).iterator
             states = state.command_states(version, command)
-            res = result(Command.State.merge_results(states))
+            res = result(states)
             range = (former_range - command_start).restrict(chunk.range)
             markup = Command.State.merge_markup(states, markup_index, range, elements)
             Text.Info(r0, a) <- markup.cumulate[A](range, info, elements,
@@ -756,12 +756,12 @@
         def select[A](
           range: Text.Range,
           elements: Elements,
-          result: Command.Results => Text.Markup => Option[A],
+          result: List[Command.State] => Text.Markup => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
-          def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
+          def result1(states: List[Command.State]): (Option[A], Text.Markup) => Option[Option[A]] =
           {
-            val res = result(results)
+            val res = result(states)
             (_: Option[A], x: Text.Markup) =>
               res(x) match {
                 case None => None
diff -r ecbdfe30bf7f -r a6f8c3566560 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Tue Apr 01 17:29:47 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Tue Apr 01 20:22:25 2014 +0200
@@ -380,13 +380,13 @@
   /* active elements */
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
-    snapshot.select(range, Rendering.active_elements, command_results =>
+    snapshot.select(range, Rendering.active_elements, command_states =>
       {
         case Text.Info(info_range, elem) =>
           if (elem.name == Markup.DIALOG) {
             elem match {
               case Protocol.Dialog(_, serial, _)
-              if !command_results.defined(serial) =>
+              if !command_states.exists(st => st.results.defined(serial)) =>
                 Some(Text.Info(snapshot.convert(info_range), elem))
               case _ => None
             }
@@ -395,12 +395,9 @@
       }).headOption.map(_.info)
 
   def command_results(range: Text.Range): Command.Results =
-  {
-    val results =
-      snapshot.select[Command.Results](range, Document.Elements.full, command_results =>
-        { case _ => Some(command_results) }).map(_.info)
-    (Command.Results.empty /: results)(_ ++ _)
-  }
+    Command.State.merge_results(
+      snapshot.select[List[Command.State]](range, Document.Elements.full, command_states =>
+        { case _ => Some(command_states) }).flatMap(_.info))
 
 
   /* tooltip messages */
@@ -606,7 +603,7 @@
         Text.Info(r, result) <-
           snapshot.cumulate[(List[Markup], Option[Color])](
             range, (List(Markup.Empty), None), Rendering.background_elements,
-            command_results =>
+            command_states =>
               {
                 case (((status, color), Text.Info(_, XML.Elem(markup, _))))
                 if !status.isEmpty && Protocol.command_status_elements(markup.name) =>
@@ -616,7 +613,9 @@
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                   Some((Nil, Some(intensify_color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
-                  command_results.get(serial) match {
+                  command_states.collectFirst(
+                    { case st if st.results.defined(serial) => st.results.get(serial).get }) match
+                  {
                     case Some(Protocol.Dialog_Result(res)) if res == result =>
                       Some((Nil, Some(active_result_color)))
                     case _ =>