# HG changeset patch
# User wenzelm
# Date 1497386397 -7200
# Node ID 3f7067ba5df35931ba80b0a3733706ce43999dae
# Parent  100f020995322bbc94a71d6dd2d10ec8897143ff
clarified signature;

diff -r 100f02099532 -r 3f7067ba5df3 src/Tools/VSCode/src/dynamic_output.scala
--- a/src/Tools/VSCode/src/dynamic_output.scala	Tue Jun 13 21:36:47 2017 +0200
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Tue Jun 13 22:39:57 2017 +0200
@@ -20,10 +20,10 @@
       val st1 =
         resources.get_caret() match {
           case None => copy(output = Nil)
-          case Some((_, model, caret_offset)) =>
-            val snapshot = model.snapshot()
+          case Some(caret) =>
+            val snapshot = caret.model.snapshot()
             if (do_update && !snapshot.is_outdated) {
-              snapshot.current_command(model.node_name, caret_offset) match {
+              snapshot.current_command(caret.node_name, caret.offset) match {
                 case None => copy(output = Nil)
                 case Some(command) =>
                   copy(output =
diff -r 100f02099532 -r 3f7067ba5df3 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Jun 13 21:36:47 2017 +0200
+++ b/src/Tools/VSCode/src/server.scala	Tue Jun 13 22:39:57 2017 +0200
@@ -433,9 +433,10 @@
     override def invoke(): Unit = delay_input.invoke()
 
     override def current_node(context: Unit): Option[Document.Node.Name] =
-      resources.get_caret().map(_._2.node_name)
+      resources.get_caret().map(_.model.node_name)
     override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
-      resources.get_caret().map(_._2.snapshot())
+      resources.get_caret().map(_.model.snapshot())
+
     override def node_snapshot(name: Document.Node.Name): Document.Snapshot =
     {
       resources.get_model(name) match {
@@ -447,8 +448,7 @@
     def current_command(snapshot: Document.Snapshot): Option[Command] =
     {
       resources.get_caret() match {
-        case Some((_, model, caret_offset)) =>
-          snapshot.current_command(model.node_name, caret_offset)
+        case Some(caret) => snapshot.current_command(caret.node_name, caret.offset)
         case None => None
       }
     }
diff -r 100f02099532 -r 3f7067ba5df3 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 13 21:36:47 2017 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Tue Jun 13 22:39:57 2017 +0200
@@ -50,6 +50,14 @@
           blob <- model.get_blob
         } yield (model.node_name -> blob)).toMap)
   }
+
+
+  /* caret */
+
+  sealed case class Caret(file: JFile, model: Document_Model, offset: Text.Offset)
+  {
+    def node_name: Document.Node.Name = model.node_name
+  }
 }
 
 class VSCode_Resources(
@@ -302,7 +310,7 @@
   def update_caret(caret: Option[(JFile, Line.Position)])
   { state.change(_.update_caret(caret)) }
 
-  def get_caret(): Option[(JFile, Document_Model, Text.Offset)] =
+  def get_caret(): Option[VSCode_Resources.Caret] =
   {
     val st = state.value
     for {
@@ -310,7 +318,7 @@
       model <- st.models.get(file)
       offset <- model.content.doc.offset(pos)
     }
-    yield (file, model, offset)
+    yield VSCode_Resources.Caret(file, model, offset)
   }