# HG changeset patch
# User wenzelm
# Date 1489322890 -3600
# Node ID ffab6f460a82c945268eda827dc939a99b8d4e43
# Parent  6dabae94cf57d0ef507e679647ee6a5984da41bf
tuned;

diff -r 6dabae94cf57 -r ffab6f460a82 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Mar 12 13:41:16 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 12 13:48:10 2017 +0100
@@ -449,6 +449,7 @@
     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 find_command(id: Document_ID.Generic): Option[(Node, Command)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
@@ -820,6 +821,9 @@
             start <- node.command_start(cmd)
           } yield convert(cmd.proper_range + start)).toList
 
+        def command_results(command: Command): Command.Results =
+          state.command_results(version, command)
+
 
         /* find command */
 
diff -r 6dabae94cf57 -r ffab6f460a82 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Sun Mar 12 13:41:16 2017 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Sun Mar 12 13:48:10 2017 +0100
@@ -78,7 +78,7 @@
       state0.location match {
         case Some(cmd) =>
           val snapshot = editor.node_snapshot(cmd.node_name)
-          val command_results = snapshot.state.command_results(snapshot.version, cmd)
+          val command_results = snapshot.command_results(cmd)
           val results =
             (for {
               (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
diff -r 6dabae94cf57 -r ffab6f460a82 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 13:41:16 2017 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 13:48:10 2017 +0100
@@ -28,8 +28,7 @@
                 case Some(command) =>
                   copy(output =
                     if (!restriction.isDefined || restriction.get.contains(command))
-                      Rendering.output_messages(
-                        snapshot.state.command_results(snapshot.version, command))
+                      Rendering.output_messages(snapshot.command_results(command))
                     else output)
               }
             }
diff -r 6dabae94cf57 -r ffab6f460a82 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Sun Mar 12 13:41:16 2017 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala	Sun Mar 12 13:48:10 2017 +0100
@@ -52,8 +52,7 @@
     } {
       val (command, results) =
         PIDE.editor.current_command(view, snapshot) match {
-          case Some(command) =>
-            (command, snapshot.state.command_results(snapshot.version, command))
+          case Some(command) => (command, snapshot.command_results(command))
           case None => (Command.empty, Command.Results.empty)
         }
 
diff -r 6dabae94cf57 -r ffab6f460a82 src/Tools/jEdit/src/simplifier_trace_dockable.scala
--- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sun Mar 12 13:41:16 2017 +0100
+++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala	Sun Mar 12 13:48:10 2017 +0100
@@ -87,7 +87,7 @@
           if (follow && !snapshot.is_outdated) {
             PIDE.editor.current_command(view, snapshot) match {
               case Some(cmd) =>
-                (snapshot, cmd, snapshot.state.command_results(snapshot.version, cmd), cmd.id)
+                (snapshot, cmd, snapshot.command_results(cmd), cmd.id)
               case None =>
                 (Document.State.init.snapshot(), Command.empty, Command.Results.empty, 0L)
             }