dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);

--- a/src/Pure/build-jars	Sat Mar 11 22:19:22 2017 +0100
+++ b/src/Pure/build-jars	Sat Mar 11 23:12:55 2017 +0100
@@ -164,6 +164,7 @@
   ../Tools/VSCode/src/build_vscode.scala
   ../Tools/VSCode/src/channel.scala
   ../Tools/VSCode/src/document_model.scala
+  ../Tools/VSCode/src/dynamic_output.scala
   ../Tools/VSCode/src/grammar.scala
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala

--- a/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 22:19:22 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Mar 11 23:12:55 2017 +0100
@@ -37,8 +37,6 @@
 const dynamic_output_type = new NotificationType<string, void>("PIDE/dynamic_output")
 
 let last_caret_update: Caret_Update = {}
-let dynamic_output: string = ""
-
 
 
 /* activate extension */
@@ -77,6 +75,11 @@
 
     /* caret handling and dynamic output */
 
+    const dynamic_output = vscode.window.createOutputChannel("Isabelle Output")
+    context.subscriptions.push(dynamic_output)
+    dynamic_output.show(true)
+    dynamic_output.hide()
+
     function update_caret()
     {
       const editor = vscode.window.activeTextEditor
@@ -95,7 +98,13 @@
 
     client.onReady().then(() =>
     {
-      client.onNotification(dynamic_output_type, body => { dynamic_output = body })
+      client.onNotification(dynamic_output_type,
+        body => {
+          if (body) {
+            dynamic_output.clear()
+            dynamic_output.appendLine(body)
+          }
+        })
       vscode.window.onDidChangeActiveTextEditor(_ => update_caret())
       vscode.window.onDidChangeTextEditorSelection(_ => update_caret())
       update_caret()

--- a/src/Tools/VSCode/src/document_model.scala	Sat Mar 11 22:19:22 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Mar 11 23:12:55 2017 +0100
@@ -158,6 +158,24 @@
   }
 
 
+  /* current command */
+
+  def current_command(snapshot: Document.Snapshot, current_offset: Text.Offset): Option[Command] =
+  {
+    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)
+      }
+      else None
+    }
+    else snapshot.version.nodes.commands_loading(node_name).headOption
+  }
+
+
   /* prover session */
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
@@ -165,5 +183,7 @@
   def is_stable: Boolean = pending_edits.isEmpty
   def snapshot(): Document.Snapshot = session.snapshot(node_name, pending_edits)
 
-  def rendering(): VSCode_Rendering = new VSCode_Rendering(this, snapshot(), resources)
+  def rendering(snapshot: Document.Snapshot): VSCode_Rendering =
+    new VSCode_Rendering(this, snapshot, resources)
+  def rendering(): VSCode_Rendering = rendering(snapshot())
 }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/dynamic_output.scala	Sat Mar 11 23:12:55 2017 +0100
@@ -0,0 +1,88 @@
+/*  Title:      Tools/VSCode/src/dynamic_output.scala
+    Author:     Makarius
+
+Dynamic output, depending on caret focus: messages, state etc.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object Dynamic_Output
+{
+  case class State(
+    do_update: Boolean = true,
+    snapshot: Document.Snapshot = Document.Snapshot.init,
+    command: Command = Command.empty,
+    results: Command.Results = Command.Results.empty,
+    output: List[XML.Tree] = Nil)
+
+  def apply(server: Server): Dynamic_Output = new Dynamic_Output(server)
+}
+
+
+class Dynamic_Output private(server: Server)
+{
+  private val state = Synchronized(Dynamic_Output.State())
+
+  private def handle_update(restriction: Option[Set[Command]])
+  {
+    state.change(st =>
+      {
+        val resources = server.resources
+        def init_st = Dynamic_Output.State(st.do_update)
+        val st1 =
+          resources.caret_range() match {
+            case None => init_st
+            case Some((model, caret_range)) =>
+              val snapshot = model.snapshot()
+              if (st.do_update && !snapshot.is_outdated) {
+                model.current_command(snapshot, caret_range.start) match {
+                  case None => init_st
+                  case Some(command) =>
+                    val results = snapshot.state.command_results(snapshot.version, command)
+                    val output =
+                      if (!restriction.isDefined || restriction.get.contains(command))
+                        Rendering.output_messages(results)
+                      else st.output
+                    st.copy(
+                      snapshot = snapshot, command = command, results = results, output = output)
+                }
+              }
+              else st
+          }
+        if (st1.output != st.output) {
+          server.channel.write(Protocol.Dynamic_Output(
+            resources.output_pretty_message(Pretty.separate(st1.output))))
+        }
+        st1
+      })
+  }
+
+
+  /* main */
+
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case changed: Session.Commands_Changed =>
+        handle_update(if (changed.assignment) None else Some(changed.commands))
+
+      case Session.Caret_Focus =>
+        handle_update(None)
+    }
+
+  def init()
+  {
+    server.session.commands_changed += main
+    server.session.caret_focus += main
+    handle_update(None)
+  }
+
+  def exit()
+  {
+    server.session.commands_changed -= main
+    server.session.caret_focus -= main
+  }
+}

--- a/src/Tools/VSCode/src/server.scala	Sat Mar 11 22:19:22 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Mar 11 23:12:55 2017 +0100
@@ -87,7 +87,7 @@
 }
 
 class Server(
-  channel: Channel,
+  val channel: Channel,
   options: Options,
   text_length: Text.Length = Text.Length.encoding(Server.default_text_length),
   session_name: String = Server.default_logic,
@@ -109,6 +109,8 @@
       offset <- model.content.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
+  private val dynamic_output = Dynamic_Output(this)
+
 
   /* input from client or file-system */
 
@@ -238,6 +240,8 @@
       catch { case ERROR(msg) => reply(msg); None }
 
     for (session <- try_session) {
+      session_.change(_ => Some(session))
+
       var session_phase: Session.Consumer[Session.Phase] = null
       session_phase =
         Session.Consumer(getClass.getName) {
@@ -255,11 +259,11 @@
       session.commands_changed += prover_output
       session.all_messages += syslog
 
+      dynamic_output.init()
+
       session.start(receiver =>
         Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
           modes = modes, receiver = receiver))
-
-      session_.change(_ => Some(session))
     }
   }
 
@@ -269,6 +273,7 @@
 
     session_.change({
       case Some(session) =>
+        dynamic_output.exit()
         var session_phase: Session.Consumer[Session.Phase] = null
         session_phase =
           Session.Consumer(getClass.getName) {

--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 22:19:22 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Mar 11 23:12:55 2017 +0100
@@ -277,17 +277,19 @@
 
   /* caret handling */
 
-  def update_caret(new_caret: Option[(JFile, Line.Position)])
-  { state.change(_.copy(caret = new_caret)) }
+  def update_caret(caret: Option[(JFile, Line.Position)])
+  { state.change(_.copy(caret = caret)) }
 
-  def caret_position: Option[(Document_Model, Line.Position)] =
+  def caret_range(): Option[(Document_Model, Text.Range)] =
   {
     val st = state.value
     for {
       (file, pos) <- st.caret
       model <- st.models.get(file)
+      offset <- model.content.doc.offset(pos)
+      if offset < model.content.doc.text_range.stop
     }
-    yield (model, pos)
+    yield (model, Text.Range(offset, offset + 1))
   }