# HG changeset patch
# User wenzelm
# Date 1395864069 -3600
# Node ID cf7710540f39afeae386ec5acaf32020669df3a4
# Parent  3925634718fb335284091dec75f9fb13302a5f58
tuned signature -- expose less intermediate information;

diff -r 3925634718fb -r cf7710540f39 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Mar 26 20:32:15 2014 +0100
+++ b/src/Pure/PIDE/document.scala	Wed Mar 26 21:01:09 2014 +0100
@@ -429,13 +429,13 @@
       range: Text.Range,
       info: A,
       elements: Elements,
-      result: Command.State => (A, Text.Markup) => Option[A],
+      result: Command.Results => (A, Text.Markup) => Option[A],
       status: Boolean = false): List[Text.Info[A]]
 
     def select[A](
       range: Text.Range,
       elements: Elements,
-      result: Command.State => Text.Markup => Option[A],
+      result: Command.Results => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
   }
 
@@ -708,7 +708,7 @@
           range: Text.Range,
           info: A,
           elements: Elements,
-          result: Command.State => (A, Text.Markup) => Option[A],
+          result: Command.Results => (A, Text.Markup) => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
           val former_range = revert(range)
@@ -719,7 +719,7 @@
               (for {
                 chunk <- thy_load_command.chunks.get(file_name).iterator
                 st = state.command_state(version, thy_load_command)
-                res = result(st)
+                res = result(st.results)
                 Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   former_range.restrict(chunk.range), info, elements,
                   { case (a, Text.Info(r0, b)) => res(a, Text.Info(convert(r0), b)) }
@@ -731,7 +731,7 @@
               (for {
                 (command, command_start) <- node.command_range(former_range)
                 st = state.command_state(version, command)
-                res = result(st)
+                res = result(st.results)
                 Text.Info(r0, a) <- st.markup(markup_index).cumulate[A](
                   (former_range - command_start).restrict(command.range), info, elements,
                   {
@@ -744,12 +744,12 @@
         def select[A](
           range: Text.Range,
           elements: Elements,
-          result: Command.State => Text.Markup => Option[A],
+          result: Command.Results => Text.Markup => Option[A],
           status: Boolean = false): List[Text.Info[A]] =
         {
-          def result1(st: Command.State): (Option[A], Text.Markup) => Option[Option[A]] =
+          def result1(results: Command.Results): (Option[A], Text.Markup) => Option[Option[A]] =
           {
-            val res = result(st)
+            val res = result(results)
             (_: Option[A], x: Text.Markup) =>
               res(x) match {
                 case None => None
diff -r 3925634718fb -r cf7710540f39 src/Tools/jEdit/src/rendering.scala
--- a/src/Tools/jEdit/src/rendering.scala	Wed Mar 26 20:32:15 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Wed Mar 26 21:01:09 2014 +0100
@@ -380,13 +380,13 @@
   /* active elements */
 
   def active(range: Text.Range): Option[Text.Info[XML.Elem]] =
-    snapshot.select(range, Rendering.active_elements, command_state =>
+    snapshot.select(range, Rendering.active_elements, command_results =>
       {
         case Text.Info(info_range, elem) =>
           if (elem.name == Markup.DIALOG) {
             elem match {
               case Protocol.Dialog(_, serial, _)
-              if !command_state.results.defined(serial) =>
+              if !command_results.defined(serial) =>
                 Some(Text.Info(snapshot.convert(info_range), elem))
               case _ => None
             }
@@ -397,8 +397,8 @@
   def command_results(range: Text.Range): Command.Results =
   {
     val results =
-      snapshot.select[Command.Results](range, Document.Elements.full, command_state =>
-        { case _ => Some(command_state.results) }).map(_.info)
+      snapshot.select[Command.Results](range, Document.Elements.full, command_results =>
+        { case _ => Some(command_results) }).map(_.info)
     (Command.Results.empty /: results)(_ ++ _)
   }
 
@@ -606,7 +606,7 @@
         Text.Info(r, result) <-
           snapshot.cumulate[(Option[Protocol.Status], Option[Color])](
             range, (Some(Protocol.Status.init), None), Rendering.background_elements,
-            command_state =>
+            command_results =>
               {
                 case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
                 if (Protocol.command_status_elements(markup.name)) =>
@@ -616,7 +616,7 @@
                 case (_, Text.Info(_, XML.Elem(Markup(Markup.INTENSIFY, _), _))) =>
                   Some((None, Some(intensify_color)))
                 case (acc, Text.Info(_, Protocol.Dialog(_, serial, result))) =>
-                  command_state.results.get(serial) match {
+                  command_results.get(serial) match {
                     case Some(Protocol.Dialog_Result(res)) if res == result =>
                       Some((None, Some(active_result_color)))
                     case _ =>