clarified current_command: index refers to node content, negative index means first command;

--- a/src/Pure/PIDE/document.scala	Sun Mar 12 14:43:50 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 12 17:59:03 2017 +0100
@@ -450,6 +450,7 @@
     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)
@@ -824,6 +825,18 @@
         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)
+            if (iterator.hasNext) {
+              val (command0, _) = iterator.next
+              other_node.commands.reverse.iterator(command0).find(command => !command.is_ignored)
+            }
+            else other_node.commands.reverse.iterator.find(command => !command.is_ignored)
+          }
+          else version.nodes.commands_loading(other_node_name).headOption
+
 
         /* find command */
 

--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:43:50 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 17:59:03 2017 +0100
@@ -159,27 +159,6 @@
   }
 
 
-  /* current command */
-
-  def current_command(snapshot: Document.Snapshot, current_offset: Text.Offset): Option[Command] =
-  {
-    if (is_theory) {
-      val node = snapshot.version.nodes(node_name)
-      val caret = snapshot.revert(current_offset)
-      if (caret < content.text_length) {
-        val caret_command_iterator = node.command_iterator(caret)
-        if (caret_command_iterator.hasNext) {
-          val (cmd0, _) = caret_command_iterator.next
-          node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
-        }
-        else None
-      }
-      else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
-    }
-    else snapshot.version.nodes.commands_loading(node_name).headOption
-  }
-
-
   /* prover session */
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]

--- a/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 14:43:50 2017 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 17:59:03 2017 +0100
@@ -23,7 +23,7 @@
           case Some((model, caret_offset)) =>
             val snapshot = model.snapshot()
             if (do_update && !snapshot.is_outdated) {
-              model.current_command(snapshot, caret_offset) match {
+              snapshot.current_command(model.node_name, caret_offset) match {
                 case None => copy(output = Nil)
                 case Some(command) =>
                   copy(output =

--- a/src/Tools/jEdit/src/jedit_editor.scala	Sun Mar 12 14:43:50 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sun Mar 12 17:59:03 2017 +0100
@@ -75,17 +75,7 @@
 
     Document_View.get(text_area) match {
       case Some(doc_view) if doc_view.model.is_theory =>
-        val node = snapshot.version.nodes(doc_view.model.node_name)
-        val caret = snapshot.revert(text_area.getCaretPosition)
-        if (caret < buffer.getLength) {
-          val caret_command_iterator = node.command_iterator(caret)
-          if (caret_command_iterator.hasNext) {
-            val (cmd0, _) = caret_command_iterator.next
-            node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored)
-          }
-          else None
-        }
-        else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
+        snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition)
       case _ =>
         Document_Model.get(buffer) match {
           case Some(model) if !model.is_theory =>