--- 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
}
--- 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 =
--- 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)
}