# HG changeset patch
# User wenzelm
# Date 1489326230 -3600
# Node ID 76cef38242d278bad6390531f402ec4825b07d10
# Parent  8fada74d82bed1003d33a7ff72203541d25f3876
clarified caret offset;
show output at end of file;

diff -r 8fada74d82be -r 76cef38242d2 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:31:29 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:43:50 2017 +0100
@@ -166,12 +166,15 @@
     if (is_theory) {
       val node = snapshot.version.nodes(node_name)
       val caret = snapshot.revert(current_offset)
-      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)
+      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 None
+      else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored)
     }
     else snapshot.version.nodes.commands_loading(node_name).headOption
   }
diff -r 8fada74d82be -r 76cef38242d2 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 14:31:29 2017 +0100
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sun Mar 12 14:43:50 2017 +0100
@@ -18,12 +18,12 @@
       resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =
     {
       val st1 =
-        resources.caret_range() match {
+        resources.caret_offset() match {
           case None => copy(output = Nil)
-          case Some((model, caret_range)) =>
+          case Some((model, caret_offset)) =>
             val snapshot = model.snapshot()
             if (do_update && !snapshot.is_outdated) {
-              model.current_command(snapshot, caret_range.start) match {
+              model.current_command(snapshot, caret_offset) match {
                 case None => copy(output = Nil)
                 case Some(command) =>
                   copy(output =
diff -r 8fada74d82be -r 76cef38242d2 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 14:31:29 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sun Mar 12 14:43:50 2017 +0100
@@ -279,16 +279,15 @@
   def update_caret(caret: Option[(JFile, Line.Position)])
   { state.change(_.copy(caret = caret)) }
 
-  def caret_range(): Option[(Document_Model, Text.Range)] =
+  def caret_offset(): Option[(Document_Model, Text.Offset)] =
   {
     val st = state.value
     for {
       (file, pos) <- st.caret
       model <- st.models.get(file)
       offset <- model.content.doc.offset(pos)
-      if offset < model.content.text_length
     }
-    yield (model, Text.Range(offset, offset + 1))
+    yield (model, offset)
   }