# HG changeset patch
# User wenzelm
# Date 1496173118 -7200
# Node ID 1448d71fbd2293506ba86df099b1605b54b1a2c6
# Parent  f20739a63a44159ac1bef7c4adb7c16f1b0ef2ff
tuned signature;

diff -r f20739a63a44 -r 1448d71fbd22 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue May 30 19:25:06 2017 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Tue May 30 21:38:38 2017 +0200
@@ -18,9 +18,9 @@
       resources: VSCode_Resources, channel: Channel, restriction: Option[Set[Command]]): State =
     {
       val st1 =
-        resources.caret_offset() match {
+        resources.get_caret() match {
           case None => copy(output = Nil)
-          case Some((model, caret_offset)) =>
+          case Some((_, model, caret_offset)) =>
             val snapshot = model.snapshot()
             if (do_update && !snapshot.is_outdated) {
               snapshot.current_command(model.node_name, caret_offset) match {
diff -r f20739a63a44 -r 1448d71fbd22 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue May 30 19:25:06 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue May 30 21:38:38 2017 +0200
@@ -302,7 +302,7 @@
   def update_caret(caret: Option[(JFile, Line.Position)])
   { state.change(_.update_caret(caret)) }
 
-  def caret_offset(): Option[(Document_Model, Text.Offset)] =
+  def get_caret(): Option[(JFile, Document_Model, Text.Offset)] =
   {
     val st = state.value
     for {
@@ -310,7 +310,7 @@
       model <- st.models.get(file)
       offset <- model.content.doc.offset(pos)
     }
-    yield (model, offset)
+    yield (file, model, offset)
   }