# HG changeset patch
# User wenzelm
# Date 1490016975 -3600
# Node ID 7dbb780f24a9b682926e9f9193423110f63e7767
# Parent  999864cdf96cbb548e43bf3a53ea53f577eb11cc
tuned signature;

diff -r 999864cdf96c -r 7dbb780f24a9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Mar 20 14:25:06 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Mar 20 14:36:15 2017 +0100
@@ -449,7 +449,6 @@
     def node: Node
     def commands_loading: List[Command]
     def commands_loading_ranges(pred: Node.Name => Boolean): List[Text.Range]
-    def command_results(command: Command): Command.Results
     def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command]
 
     def find_command(id: Document_ID.Generic): Option[(Node, Command)]
@@ -468,6 +467,9 @@
       elements: Markup.Elements,
       result: List[Command.State] => Text.Markup => Option[A],
       status: Boolean = false): List[Text.Info[A]]
+
+    def command_results(range: Text.Range): Command.Results
+    def command_results(command: Command): Command.Results
   }
 
 
@@ -827,9 +829,6 @@
             start <- node.command_start(cmd)
           } yield convert(cmd.proper_range + start)).toList
 
-        def command_results(command: Command): Command.Results =
-          state.command_results(version, command)
-
         def current_command(other_node_name: Node.Name, offset: Text.Offset): Option[Command] =
           if (other_node_name.is_theory) {
             val other_node = version.nodes(other_node_name)
@@ -919,6 +918,17 @@
         }
 
 
+        /* command results */
+
+        def command_results(range: Text.Range): Command.Results =
+          Command.State.merge_results(
+            select[List[Command.State]](range, Markup.Elements.full, command_states =>
+              { case _ => Some(command_states) }).flatMap(_.info))
+
+        def command_results(command: Command): Command.Results =
+          state.command_results(version, command)
+
+
         /* output */
 
         override def toString: String =
diff -r 999864cdf96c -r 7dbb780f24a9 src/Tools/jEdit/src/jedit_rendering.scala
--- a/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 20 14:25:06 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Mon Mar 20 14:36:15 2017 +0100
@@ -353,11 +353,6 @@
           else Some(Text.Info(snapshot.convert(info_range), elem))
       }).headOption.map(_.info)
 
-  def command_results(range: Text.Range): Command.Results =
-    Command.State.merge_results(
-      snapshot.select[List[Command.State]](range, Markup.Elements.full, command_states =>
-        { case _ => Some(command_states) }).flatMap(_.info))
-
 
   /* tooltips */
 
diff -r 999864cdf96c -r 7dbb780f24a9 src/Tools/jEdit/src/rich_text_area.scala
--- a/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 20 14:25:06 2017 +0100
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Mon Mar 20 14:36:15 2017 +0100
@@ -271,7 +271,7 @@
                         case Some(tip) =>
                           val painter = text_area.getPainter
                           val loc = new Point(x, y + painter.getLineHeight / 2)
-                          val results = rendering.command_results(tip.range)
+                          val results = snapshot.command_results(tip.range)
                           Pretty_Tooltip(view, painter, loc, rendering, results, tip)
                       }
                   }