support for caret handling and dynamic output;

--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 20:18:06 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 20:22:43 2017 +0100
@@ -24,6 +24,23 @@
 }
 
 
+/* caret handling and dynamic output */
+
+interface Caret_Update
+{
+  uri?: string
+  line?: number
+  character?: number
+}
+
+const caret_update_type = new NotificationType<Caret_Update, void>("PIDE/caret_update")
+const dynamic_output_type = new NotificationType<string, void>("PIDE/dynamic_output")
+
+let last_caret_update: Caret_Update = {}
+let dynamic_output: string = ""
+
+
+
 /* activate extension */
 
 export function activate(context: vscode.ExtensionContext)
@@ -58,6 +75,33 @@
     const client = new LanguageClient("Isabelle", server_options, client_options, false)
 
 
+    /* caret handling and dynamic output */
+
+    function update_caret()
+    {
+      const editor = vscode.window.activeTextEditor
+      let caret_update: Caret_Update = {}
+      if (editor) {
+        const uri = editor.document.uri
+        const cursor = editor.selection.active
+        if (uri.scheme === "file" && cursor)
+          caret_update = { uri: uri.toString(), line: cursor.line, character: cursor.character }
+      }
+      if (last_caret_update !== caret_update) {
+        client.sendNotification(caret_update_type, caret_update)
+        last_caret_update = caret_update
+      }
+    }
+
+    client.onReady().then(() =>
+    {
+      client.onNotification(dynamic_output_type, body => { dynamic_output = body })
+      vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
+      vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
+      update_caret()
+    })
+
+
     /* decorations */
 
     decorations.init(context)

--- a/src/Tools/VSCode/src/protocol.scala	Sat Mar 11 20:18:06 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sat Mar 11 20:22:43 2017 +0100
@@ -420,4 +420,29 @@
       Notification("PIDE/decoration",
         Map("uri" -> Url.print_file(file), "type" -> typ, "content" -> content.map(_.json)))
   }
+
+
+  /* caret handling and dynamic output */
+
+  object Caret_Update
+  {
+    def unapply(json: JSON.T): Option[Option[(JFile, Line.Position)]] =
+      json match {
+        case Notification("PIDE/caret_update", Some(params)) =>
+          val caret =
+            for {
+              uri <- JSON.string(params, "uri")
+              if Url.is_wellformed_file(uri)
+              pos <- Position.unapply(params)
+            } yield (Url.canonical_file(uri), pos)
+          Some(caret)
+        case _ => None
+      }
+  }
+
+  object Dynamic_Output
+  {
+    def apply(body: String): JSON.T =
+      Notification("PIDE/dynamic_output", body)
+  }
 }

--- a/src/Tools/VSCode/src/server.scala	Sat Mar 11 20:18:06 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Mar 11 20:22:43 2017 +0100
@@ -152,6 +152,18 @@
   }
 
 
+  /* caret handling */
+
+  private val delay_caret_update: Standard_Thread.Delay =
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay"), channel.Error_Logger)
+    { session.caret_focus.post(Session.Caret_Focus) }
+
+  private def update_caret(caret: Option[(JFile, Line.Position)])
+  {
+    resources.update_caret(caret)
+    delay_caret_update.invoke()
+  }
+
 
   /* output to client */
 
@@ -362,6 +374,7 @@
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
           case Protocol.DocumentHighlights(id, node_pos) => document_highlights(id, node_pos)
+          case Protocol.Caret_Update(caret) => update_caret(caret)
           case _ => log("### IGNORED")
         }
       }

--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 20:18:06 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 20:22:43 2017 +0100
@@ -21,7 +21,8 @@
   sealed case class State(
     models: Map[JFile, Document_Model] = Map.empty,
     pending_input: Set[JFile] = Set.empty,
-    pending_output: Set[JFile] = Set.empty)
+    pending_output: Set[JFile] = Set.empty,
+    caret: Option[(JFile, Line.Position)] = None)
   {
     def update_models(changed: Traversable[(JFile, Document_Model)]): State =
       copy(
@@ -274,6 +275,22 @@
   def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin)
 
 
+  /* caret handling */
+
+  def update_caret(new_caret: Option[(JFile, Line.Position)])
+  { state.change(_.copy(caret = new_caret)) }
+
+  def caret_position: Option[(Document_Model, Line.Position)] =
+  {
+    val st = state.value
+    for {
+      (file, pos) <- st.caret
+      model <- st.models.get(file)
+    }
+    yield (model, pos)
+  }
+
+
   /* spell checker */
 
   val spell_checker = new Spell_Checker_Variable