src/Pure/PIDE/document.scala

 
     def node_name: Node.Name
     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)]
     def find_command_position(id: Document_ID.Generic, offset: Symbol.Offset)
       : Option[Line.Node_Position]

     def select[A](
       range: Text.Range,
       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
   }
 
 
   /* model */
 

             cmd <- node.load_commands.iterator
             blob_name <- cmd.blobs_names.iterator
             if pred(blob_name)
             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)
             val iterator = other_node.command_iterator(revert(offset) max 0)

           for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1 _, status))
             yield Text.Info(r, x)
         }
 
 
+        /* 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 =
           "Snapshot(node = " + node_name.node + ", version = " + version.id +
             (if (is_outdated) ", outdated" else "") + ")"