# HG changeset patch
# User wenzelm
# Date 1497703943 -7200
# Node ID 8ff7fd4ee9197edc0d0da8b3dfda8ba9a51b3939
# Parent  def95e0bc529e3c1693bc398eafe33e3ce4dfe60# Parent  3e2145cf3077eb004437cd8402842647476f8434
merged

diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -33,6 +33,7 @@
 
   private val thread = Standard_Thread.fork(name, daemon) { main_loop(Nil) }
   def is_active: Boolean = active && thread.isAlive
+  def check_thread: Boolean = Thread.currentThread == thread
 
   private def failure(exn: Throwable): Unit =
     Output.error_message(
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/GUI/gui_thread.scala
--- a/src/Pure/GUI/gui_thread.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/GUI/gui_thread.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -14,13 +14,13 @@
 {
   /* context check */
 
-  def assert[A](body: => A) =
+  def assert[A](body: => A): A =
   {
     Predef.assert(SwingUtilities.isEventDispatchThread())
     body
   }
 
-  def require[A](body: => A) =
+  def require[A](body: => A): A =
   {
     Predef.require(SwingUtilities.isEventDispatchThread())
     body
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/PIDE/editor.scala
--- a/src/Pure/PIDE/editor.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/PIDE/editor.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -14,6 +14,10 @@
   def session: Session
   def flush(): Unit
   def invoke(): Unit
+
+
+  /* current situation */
+
   def current_node(context: Context): Option[Document.Node.Name]
   def current_node_snapshot(context: Context): Option[Document.Snapshot]
   def node_snapshot(name: Document.Node.Name): Document.Snapshot
@@ -22,16 +26,9 @@
 
   /* overlays */
 
-  private val overlays = Synchronized(Document.Overlays.empty)
-
-  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
-    overlays.value(name)
-
-  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
-    overlays.change(_.insert(command, fn, args))
-
-  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
-    overlays.change(_.remove(command, fn, args))
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays
+  def insert_overlay(command: Command, fn: String, args: List[String])
+  def remove_overlay(command: Command, fn: String, args: List[String])
 
 
   /* hyperlinks */
@@ -45,4 +42,12 @@
   def hyperlink_command(
     focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
       : Option[Hyperlink]
+
+
+  /* dispatcher thread */
+
+  def assert_dispatcher[A](body: => A): A
+  def require_dispatcher[A](body: => A): A
+  def send_dispatcher(body: => Unit): Unit
+  def send_wait_dispatcher(body: => Unit): Unit
 }
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/PIDE/query_operation.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -48,7 +48,7 @@
   private val print_function = operation_name + "_query"
 
 
-  /* implicit state -- owned by GUI thread */
+  /* implicit state -- owned by editor thread */
 
   private val current_state = Synchronized(Query_Operation.State.empty)
 
@@ -67,7 +67,7 @@
 
   private def content_update()
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
 
     /* snapshot */
@@ -174,11 +174,11 @@
   /* query operations */
 
   def cancel_query(): Unit =
-    GUI_Thread.require { editor.session.cancel_exec(current_state.value.exec_id) }
+    editor.require_dispatcher { editor.session.cancel_exec(current_state.value.exec_id) }
 
   def apply_query(query: List[String])
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
     editor.current_node_snapshot(editor_context) match {
       case Some(snapshot) =>
@@ -202,7 +202,7 @@
 
   def locate_query()
   {
-    GUI_Thread.require {}
+    editor.require_dispatcher {}
 
     val state = current_state.value
     for {
@@ -224,7 +224,7 @@
           if state.update_pending ||
             (state.status != Query_Operation.Status.FINISHED &&
               changed.commands.contains(command)) =>
-            GUI_Thread.later { content_update() }
+            editor.send_dispatcher { content_update() }
           case _ =>
         }
     }
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -136,11 +136,38 @@
   def reparse_limit: Int = session_options.int("editor_reparse_limit")
 
 
-  /* outlets */
+  /* dispatcher */
 
   private val dispatcher =
     Consumer_Thread.fork[() => Unit]("Session.dispatcher", daemon = true) { case e => e(); true }
 
+  def assert_dispatcher[A](body: => A): A =
+  {
+    assert(dispatcher.check_thread)
+    body
+  }
+
+  def require_dispatcher[A](body: => A): A =
+  {
+    require(dispatcher.check_thread)
+    body
+  }
+
+  def send_dispatcher(body: => Unit): Unit =
+  {
+    if (dispatcher.check_thread) body
+    else dispatcher.send(() => body)
+  }
+
+  def send_wait_dispatcher(body: => Unit): Unit =
+  {
+    if (dispatcher.check_thread) body
+    else dispatcher.send_wait(() => body)
+  }
+
+
+  /* outlets */
+
   val statistics = new Session.Outlet[Session.Statistics](dispatcher)
   val global_options = new Session.Outlet[Session.Global_Options](dispatcher)
   val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher)
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Pure/build-jars
--- a/src/Pure/build-jars	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Pure/build-jars	Sat Jun 17 14:52:23 2017 +0200
@@ -168,9 +168,10 @@
   ../Tools/VSCode/src/document_model.scala
   ../Tools/VSCode/src/dynamic_output.scala
   ../Tools/VSCode/src/grammar.scala
-  ../Tools/VSCode/src/preview.scala
+  ../Tools/VSCode/src/preview_panel.scala
   ../Tools/VSCode/src/protocol.scala
   ../Tools/VSCode/src/server.scala
+  ../Tools/VSCode/src/state_panel.scala
   ../Tools/VSCode/src/vscode_rendering.scala
   ../Tools/VSCode/src/vscode_resources.scala
 )
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/package.json
--- a/src/Tools/VSCode/extension/package.json	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/package.json	Sat Jun 17 14:52:23 2017 +0200
@@ -8,14 +8,20 @@
         "mathematical logic",
         "functional programming",
         "document preparation"
-        ],
+    ],
     "icon": "isabelle.png",
-    "version": "0.14.0",
+    "version": "0.15.0",
     "publisher": "makarius",
     "license": "MIT",
-    "repository": { "url": "http://isabelle.in.tum.de/repos/isabelle" },
-    "engines": { "vscode": "^1.8.0" },
-    "categories": ["Languages"],
+    "repository": {
+        "url": "http://isabelle.in.tum.de/repos/isabelle"
+    },
+    "engines": {
+        "vscode": "^1.8.0"
+    },
+    "categories": [
+        "Languages"
+    ],
     "activationEvents": [
         "onLanguage:isabelle",
         "onLanguage:isabelle-ml",
@@ -27,6 +33,11 @@
     "contributes": {
         "commands": [
             {
+                "command": "isabelle.state",
+                "title": "Show Proof State",
+                "category": "Isabelle"
+            },
+            {
                 "command": "isabelle.preview",
                 "title": "Open Preview",
                 "category": "Isabelle",
@@ -97,17 +108,26 @@
         "languages": [
             {
                 "id": "isabelle",
-                "aliases": ["Isabelle"],
-                "extensions": [".thy"],
+                "aliases": [
+                    "Isabelle"
+                ],
+                "extensions": [
+                    ".thy"
+                ],
                 "configuration": "./isabelle-language.json"
             },
             {
                 "id": "isabelle-ml",
-                "aliases": ["Isabelle/ML"],
-                "extensions": [".ML", ".sml", ".sig"],
+                "aliases": [
+                    "Isabelle/ML"
+                ],
+                "extensions": [
+                    ".ML",
+                    ".sml",
+                    ".sig"
+                ],
                 "configuration": "./isabelle-ml-language.json"
             }
-
         ],
         "grammars": [
             {
@@ -131,7 +151,9 @@
                 },
                 "isabelle.args": {
                     "type": "array",
-                    "items": { "type": "string" },
+                    "items": {
+                        "type": "string"
+                    },
                     "default": [],
                     "description": "Command-line arguments for isabelle vscode_server process."
                 },
@@ -140,80 +162,302 @@
                     "default": "",
                     "description": "Cygwin installation on Windows (only relevant when running directly from the Isabelle repository)."
                 },
-                "isabelle.unprocessed_light_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" },
-                "isabelle.unprocessed_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" },
-                "isabelle.unprocessed1_light_color": { "type": "string", "default": "rgba(255, 160, 160, 0.20)" },
-                "isabelle.unprocessed1_dark_color": { "type": "string", "default": "rgba(97, 0, 97, 0.20)" },
-                "isabelle.running_light_color": { "type": "string", "default": "rgba(97, 0, 97, 1.00)" },
-                "isabelle.running_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 1.00)" },
-                "isabelle.running1_light_color": { "type": "string", "default": "rgba(97, 0, 97, 0.40)" },
-                "isabelle.running1_dark_color": { "type": "string", "default": "rgba(255, 160, 160, 0.40)" },
-                "isabelle.bad_light_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" },
-                "isabelle.bad_dark_color": { "type": "string", "default": "rgba(255, 106, 106, 0.40)" },
-                "isabelle.intensify_light_color": { "type": "string", "default": "rgba(255, 204, 102, 0.40)" },
-                "isabelle.intensify_dark_color": { "type": "string", "default": "rgba(204, 136, 0, 0.20)" },
-                "isabelle.markdown_item1_light_color": { "type": "string", "default": "rgba(218, 254, 218, 1.00)" },
-                "isabelle.markdown_item1_dark_color": { "type": "string", "default": "rgba(5, 199, 5, 0.20)" },
-                "isabelle.markdown_item2_light_color": { "type": "string", "default": "rgba(255, 240, 204, 1.00)" },
-                "isabelle.markdown_item2_dark_color": { "type": "string", "default": "rgba(204, 143, 0, 0.20)" },
-                "isabelle.markdown_item3_light_color": { "type": "string", "default": "rgba(231, 231, 255, 1.00)" },
-                "isabelle.markdown_item3_dark_color": { "type": "string", "default": "rgba(0, 0, 204, 0.20)" },
-                "isabelle.markdown_item4_light_color": { "type": "string", "default": "rgba(255, 224, 240, 1.00)" },
-                "isabelle.markdown_item4_dark_color": { "type": "string", "default": "rgba(204, 0, 105, 0.20)" },
-                "isabelle.quoted_light_color": { "type": "string", "default": "rgba(139, 139, 139, 0.10)" },
-                "isabelle.quoted_dark_color": { "type": "string", "default": "rgba(150, 150, 150, 0.15)" },
-                "isabelle.antiquoted_light_color": { "type": "string", "default": "rgba(255, 200, 50, 0.10)" },
-                "isabelle.antiquoted_dark_color": { "type": "string", "default": "rgba(255, 214, 102, 0.15)" },
-                "isabelle.writeln_light_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
-                "isabelle.writeln_dark_color": { "type": "string", "default": "rgba(192, 192, 192, 1.0)" },
-                "isabelle.information_light_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
-                "isabelle.information_dark_color": { "type": "string", "default": "rgba(193, 223, 238, 1.0)" },
-                "isabelle.warning_light_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
-                "isabelle.warning_dark_color": { "type": "string", "default": "rgba(255, 140, 0, 1.0)" },
-                "isabelle.error_light_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" },
-                "isabelle.error_dark_color": { "type": "string", "default": "rgba(178, 34, 34, 1.00)" },
-                "isabelle.spell_checker_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.0)" },
-                "isabelle.spell_checker_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" },
-                "isabelle.main_light_color": { "type": "string", "default": "rgba(0, 0, 0, 1.00)" },
-                "isabelle.main_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" },
-                "isabelle.keyword1_light_color": { "type": "string", "default": "rgba(175, 0, 219, 1.00)" },
-                "isabelle.keyword1_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" },
-                "isabelle.keyword2_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" },
-                "isabelle.keyword2_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" },
-                "isabelle.keyword3_light_color": { "type": "string", "default": "rgba(38, 127, 153, 1.00)" },
-                "isabelle.keyword3_dark_color": { "type": "string", "default": "rgba(78, 201, 176), 1.00)" },
-                "isabelle.quasi_keyword_light_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
-                "isabelle.quasi_keyword_dark_color": { "type": "string", "default": "rgba(153, 102, 255, 1.00)" },
-                "isabelle.improper_light_color": { "type": "string", "default": "rgba(205, 49, 49, 1.00)" },
-                "isabelle.improper_dark_color": { "type": "string", "default": "rgba(244, 71, 71, 1.00)" },
-                "isabelle.operator_light_color": { "type": "string", "default": "rgba(50, 50, 50, 1.00)" },
-                "isabelle.operator_dark_color": { "type": "string", "default": "rgba(212, 212, 212, 1.00)" },
-                "isabelle.tfree_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
-                "isabelle.tfree_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
-                "isabelle.tvar_light_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
-                "isabelle.tvar_dark_color": { "type": "string", "default": "rgba(160, 32, 240, 1.00)" },
-                "isabelle.free_light_color": { "type": "string", "default": "rgba(0, 0, 255, 1.00)" },
-                "isabelle.free_dark_color": { "type": "string", "default": "rgba(86, 156, 214, 1.00)" },
-                "isabelle.skolem_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
-                "isabelle.skolem_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
-                "isabelle.bound_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
-                "isabelle.bound_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" },
-                "isabelle.var_light_color": { "type": "string", "default": "rgba(0, 16, 128, 1.00)" },
-                "isabelle.var_dark_color": { "type": "string", "default": "rgba(156, 220, 254, 1.00)" },
-                "isabelle.inner_numeral_light_color": { "type": "string", "default": "rgba(9, 136, 90, 1.00)" },
-                "isabelle.inner_numeral_dark_color": { "type": "string", "default": "rgba(181, 206, 168, 1.00)" },
-                "isabelle.inner_quoted_light_color": { "type": "string", "default": "rgba(163, 21, 21, 1.00)" },
-                "isabelle.inner_quoted_dark_color": { "type": "string", "default": "rgba(206, 145, 120, 1.00)" },
-                "isabelle.inner_cartouche_light_color": { "type": "string", "default": "rgba(129, 31, 63, 1.00)" },
-                "isabelle.inner_cartouche_dark_color": { "type": "string", "default": "rgba(209, 105, 105, 1.00)" },
-                "isabelle.inner_comment_light_color": { "type": "string", "default": "rgba(0, 128, 0, 1.00)" },
-                "isabelle.inner_comment_dark_color": { "type": "string", "default": "rgba(96, 139, 78, 1.00)" },
-                "isabelle.dynamic_light_color": { "type": "string", "default": "rgba(121, 94, 38, 1.00)" },
-                "isabelle.dynamic_dark_color": { "type": "string", "default": "rgba(220, 220, 170, 1.00)" },
-                "isabelle.class_parameter_light_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
-                "isabelle.class_parameter_dark_color": { "type": "string", "default": "rgba(210, 105, 30, 1.00)" },
-                "isabelle.antiquote_light_color": { "type": "string", "default": "rgba(102, 0, 204, 1.00)" },
-                "isabelle.antiquote_dark_color": { "type": "string", "default": "rgba(197, 134, 192, 1.00)" }
+                "isabelle.unprocessed_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 160, 160, 1.00)"
+                },
+                "isabelle.unprocessed_dark_color": {
+                    "type": "string",
+                    "default": "rgba(97, 0, 97, 1.00)"
+                },
+                "isabelle.unprocessed1_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 160, 160, 0.20)"
+                },
+                "isabelle.unprocessed1_dark_color": {
+                    "type": "string",
+                    "default": "rgba(97, 0, 97, 0.20)"
+                },
+                "isabelle.running_light_color": {
+                    "type": "string",
+                    "default": "rgba(97, 0, 97, 1.00)"
+                },
+                "isabelle.running_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 160, 160, 1.00)"
+                },
+                "isabelle.running1_light_color": {
+                    "type": "string",
+                    "default": "rgba(97, 0, 97, 0.40)"
+                },
+                "isabelle.running1_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 160, 160, 0.40)"
+                },
+                "isabelle.bad_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 106, 106, 0.40)"
+                },
+                "isabelle.bad_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 106, 106, 0.40)"
+                },
+                "isabelle.intensify_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 204, 102, 0.40)"
+                },
+                "isabelle.intensify_dark_color": {
+                    "type": "string",
+                    "default": "rgba(204, 136, 0, 0.20)"
+                },
+                "isabelle.markdown_item1_light_color": {
+                    "type": "string",
+                    "default": "rgba(218, 254, 218, 1.00)"
+                },
+                "isabelle.markdown_item1_dark_color": {
+                    "type": "string",
+                    "default": "rgba(5, 199, 5, 0.20)"
+                },
+                "isabelle.markdown_item2_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 240, 204, 1.00)"
+                },
+                "isabelle.markdown_item2_dark_color": {
+                    "type": "string",
+                    "default": "rgba(204, 143, 0, 0.20)"
+                },
+                "isabelle.markdown_item3_light_color": {
+                    "type": "string",
+                    "default": "rgba(231, 231, 255, 1.00)"
+                },
+                "isabelle.markdown_item3_dark_color": {
+                    "type": "string",
+                    "default": "rgba(0, 0, 204, 0.20)"
+                },
+                "isabelle.markdown_item4_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 224, 240, 1.00)"
+                },
+                "isabelle.markdown_item4_dark_color": {
+                    "type": "string",
+                    "default": "rgba(204, 0, 105, 0.20)"
+                },
+                "isabelle.quoted_light_color": {
+                    "type": "string",
+                    "default": "rgba(139, 139, 139, 0.10)"
+                },
+                "isabelle.quoted_dark_color": {
+                    "type": "string",
+                    "default": "rgba(150, 150, 150, 0.15)"
+                },
+                "isabelle.antiquoted_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 200, 50, 0.10)"
+                },
+                "isabelle.antiquoted_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 214, 102, 0.15)"
+                },
+                "isabelle.writeln_light_color": {
+                    "type": "string",
+                    "default": "rgba(192, 192, 192, 1.0)"
+                },
+                "isabelle.writeln_dark_color": {
+                    "type": "string",
+                    "default": "rgba(192, 192, 192, 1.0)"
+                },
+                "isabelle.information_light_color": {
+                    "type": "string",
+                    "default": "rgba(193, 223, 238, 1.0)"
+                },
+                "isabelle.information_dark_color": {
+                    "type": "string",
+                    "default": "rgba(193, 223, 238, 1.0)"
+                },
+                "isabelle.warning_light_color": {
+                    "type": "string",
+                    "default": "rgba(255, 140, 0, 1.0)"
+                },
+                "isabelle.warning_dark_color": {
+                    "type": "string",
+                    "default": "rgba(255, 140, 0, 1.0)"
+                },
+                "isabelle.error_light_color": {
+                    "type": "string",
+                    "default": "rgba(178, 34, 34, 1.00)"
+                },
+                "isabelle.error_dark_color": {
+                    "type": "string",
+                    "default": "rgba(178, 34, 34, 1.00)"
+                },
+                "isabelle.spell_checker_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 0, 255, 1.0)"
+                },
+                "isabelle.spell_checker_dark_color": {
+                    "type": "string",
+                    "default": "rgba(86, 156, 214, 1.00)"
+                },
+                "isabelle.main_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 0, 0, 1.00)"
+                },
+                "isabelle.main_dark_color": {
+                    "type": "string",
+                    "default": "rgba(212, 212, 212, 1.00)"
+                },
+                "isabelle.keyword1_light_color": {
+                    "type": "string",
+                    "default": "rgba(175, 0, 219, 1.00)"
+                },
+                "isabelle.keyword1_dark_color": {
+                    "type": "string",
+                    "default": "rgba(197, 134, 192, 1.00)"
+                },
+                "isabelle.keyword2_light_color": {
+                    "type": "string",
+                    "default": "rgba(9, 136, 90, 1.00)"
+                },
+                "isabelle.keyword2_dark_color": {
+                    "type": "string",
+                    "default": "rgba(181, 206, 168, 1.00)"
+                },
+                "isabelle.keyword3_light_color": {
+                    "type": "string",
+                    "default": "rgba(38, 127, 153, 1.00)"
+                },
+                "isabelle.keyword3_dark_color": {
+                    "type": "string",
+                    "default": "rgba(78, 201, 176), 1.00)"
+                },
+                "isabelle.quasi_keyword_light_color": {
+                    "type": "string",
+                    "default": "rgba(153, 102, 255, 1.00)"
+                },
+                "isabelle.quasi_keyword_dark_color": {
+                    "type": "string",
+                    "default": "rgba(153, 102, 255, 1.00)"
+                },
+                "isabelle.improper_light_color": {
+                    "type": "string",
+                    "default": "rgba(205, 49, 49, 1.00)"
+                },
+                "isabelle.improper_dark_color": {
+                    "type": "string",
+                    "default": "rgba(244, 71, 71, 1.00)"
+                },
+                "isabelle.operator_light_color": {
+                    "type": "string",
+                    "default": "rgba(50, 50, 50, 1.00)"
+                },
+                "isabelle.operator_dark_color": {
+                    "type": "string",
+                    "default": "rgba(212, 212, 212, 1.00)"
+                },
+                "isabelle.tfree_light_color": {
+                    "type": "string",
+                    "default": "rgba(160, 32, 240, 1.00)"
+                },
+                "isabelle.tfree_dark_color": {
+                    "type": "string",
+                    "default": "rgba(160, 32, 240, 1.00)"
+                },
+                "isabelle.tvar_light_color": {
+                    "type": "string",
+                    "default": "rgba(160, 32, 240, 1.00)"
+                },
+                "isabelle.tvar_dark_color": {
+                    "type": "string",
+                    "default": "rgba(160, 32, 240, 1.00)"
+                },
+                "isabelle.free_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 0, 255, 1.00)"
+                },
+                "isabelle.free_dark_color": {
+                    "type": "string",
+                    "default": "rgba(86, 156, 214, 1.00)"
+                },
+                "isabelle.skolem_light_color": {
+                    "type": "string",
+                    "default": "rgba(210, 105, 30, 1.00)"
+                },
+                "isabelle.skolem_dark_color": {
+                    "type": "string",
+                    "default": "rgba(210, 105, 30, 1.00)"
+                },
+                "isabelle.bound_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 128, 0, 1.00)"
+                },
+                "isabelle.bound_dark_color": {
+                    "type": "string",
+                    "default": "rgba(96, 139, 78, 1.00)"
+                },
+                "isabelle.var_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 16, 128, 1.00)"
+                },
+                "isabelle.var_dark_color": {
+                    "type": "string",
+                    "default": "rgba(156, 220, 254, 1.00)"
+                },
+                "isabelle.inner_numeral_light_color": {
+                    "type": "string",
+                    "default": "rgba(9, 136, 90, 1.00)"
+                },
+                "isabelle.inner_numeral_dark_color": {
+                    "type": "string",
+                    "default": "rgba(181, 206, 168, 1.00)"
+                },
+                "isabelle.inner_quoted_light_color": {
+                    "type": "string",
+                    "default": "rgba(163, 21, 21, 1.00)"
+                },
+                "isabelle.inner_quoted_dark_color": {
+                    "type": "string",
+                    "default": "rgba(206, 145, 120, 1.00)"
+                },
+                "isabelle.inner_cartouche_light_color": {
+                    "type": "string",
+                    "default": "rgba(129, 31, 63, 1.00)"
+                },
+                "isabelle.inner_cartouche_dark_color": {
+                    "type": "string",
+                    "default": "rgba(209, 105, 105, 1.00)"
+                },
+                "isabelle.inner_comment_light_color": {
+                    "type": "string",
+                    "default": "rgba(0, 128, 0, 1.00)"
+                },
+                "isabelle.inner_comment_dark_color": {
+                    "type": "string",
+                    "default": "rgba(96, 139, 78, 1.00)"
+                },
+                "isabelle.dynamic_light_color": {
+                    "type": "string",
+                    "default": "rgba(121, 94, 38, 1.00)"
+                },
+                "isabelle.dynamic_dark_color": {
+                    "type": "string",
+                    "default": "rgba(220, 220, 170, 1.00)"
+                },
+                "isabelle.class_parameter_light_color": {
+                    "type": "string",
+                    "default": "rgba(210, 105, 30, 1.00)"
+                },
+                "isabelle.class_parameter_dark_color": {
+                    "type": "string",
+                    "default": "rgba(210, 105, 30, 1.00)"
+                },
+                "isabelle.antiquote_light_color": {
+                    "type": "string",
+                    "default": "rgba(102, 0, 204, 1.00)"
+                },
+                "isabelle.antiquote_dark_color": {
+                    "type": "string",
+                    "default": "rgba(197, 134, 192, 1.00)"
+                }
             }
         }
     },
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/content_provider.ts
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/extension/src/content_provider.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -0,0 +1,35 @@
+'use strict'
+
+import { Event, EventEmitter, Uri, TextDocumentContentProvider, Disposable,
+  workspace } from 'vscode'
+
+
+export class Content_Provider implements TextDocumentContentProvider
+{
+  private _uri_template: Uri
+  get uri_template(): Uri { return this._uri_template }
+  get uri_scheme(): string { return this.uri_template.scheme }
+
+  constructor(uri_scheme: string)
+  {
+    this._uri_template = Uri.parse("scheme:").with({ scheme: uri_scheme })
+  }
+  dispose() { }
+
+  private emitter = new EventEmitter<Uri>()
+  public update(uri: Uri) { this.emitter.fire(uri) }
+  get onDidChange(): Event<Uri> { return this.emitter.event }
+
+  private content = new Map<string, string>()
+  public set_content(uri: Uri, content: string) { this.content.set(uri.toString(), content)}
+
+  provideTextDocumentContent(uri: Uri): string
+  {
+    return this.content.get(uri.toString()) || ""
+  }
+
+  public register(): Disposable
+  {
+    return workspace.registerTextDocumentContentProvider(this.uri_scheme, this)
+  }
+}
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/decorations.ts
--- a/src/Tools/VSCode/extension/src/decorations.ts	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/src/decorations.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -65,11 +65,11 @@
 ]
 
 
-/* init */
+/* setup */
 
 const types = new Map<string, TextEditorDecorationType>()
 
-export function init(context: ExtensionContext)
+export function setup(context: ExtensionContext)
 {
   function decoration(options: DecorationRenderOptions): TextEditorDecorationType
   {
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/extension.ts
--- a/src/Tools/VSCode/extension/src/extension.ts	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/src/extension.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -4,8 +4,9 @@
 import * as fs from 'fs';
 import * as library from './library'
 import * as decorations from './decorations';
-import * as preview from './preview';
+import * as preview_panel from './preview_panel';
 import * as protocol from './protocol';
+import * as state_panel from './state_panel';
 import * as symbol from './symbol';
 import * as completion from './completion';
 import { ExtensionContext, workspace, window, commands, languages } from 'vscode';
@@ -48,9 +49,9 @@
 
     /* decorations */
 
-    decorations.init(context)
+    decorations.setup(context)
     context.subscriptions.push(
-      workspace.onDidChangeConfiguration(() => decorations.init(context)),
+      workspace.onDidChangeConfiguration(() => decorations.setup(context)),
       workspace.onDidChangeTextDocument(event => decorations.touch_document(event.document)),
       window.onDidChangeActiveTextEditor(decorations.update_editor),
       workspace.onDidCloseTextDocument(decorations.close_document))
@@ -101,15 +102,25 @@
     })
 
 
-    /* preview */
+    /* state panel */
 
     context.subscriptions.push(
-      commands.registerCommand("isabelle.preview", uri => preview.request(uri, false)),
-      commands.registerCommand("isabelle.preview-split", uri => preview.request(uri, true)),
-      commands.registerCommand("isabelle.preview-source", preview.source),
-      commands.registerCommand("isabelle.preview-update", preview.update))
+      commands.registerCommand("isabelle.state", uri => state_panel.init(uri)),
+      commands.registerCommand("_isabelle.state-locate", state_panel.locate),
+      commands.registerCommand("_isabelle.state-update", state_panel.update))
+
+    language_client.onReady().then(() => state_panel.setup(context, language_client))
+
 
-    language_client.onReady().then(() => preview.init(context, language_client))
+    /* preview panel */
+
+    context.subscriptions.push(
+      commands.registerCommand("isabelle.preview", uri => preview_panel.request(uri, false)),
+      commands.registerCommand("isabelle.preview-split", uri => preview_panel.request(uri, true)),
+      commands.registerCommand("isabelle.preview-source", preview_panel.source),
+      commands.registerCommand("isabelle.preview-update", preview_panel.update))
+
+    language_client.onReady().then(() => preview_panel.setup(context, language_client))
 
 
     /* Isabelle symbols */
@@ -117,7 +128,7 @@
     language_client.onReady().then(() =>
     {
       language_client.onNotification(protocol.symbols_type,
-        params => symbol.init(context, params.entries))
+        params => symbol.setup(context, params.entries))
       language_client.sendNotification(protocol.symbols_request_type)
     })
 
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/preview.ts
--- a/src/Tools/VSCode/extension/src/preview.ts	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/src/preview.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -6,69 +6,45 @@
   window, commands } from 'vscode'
 import { LanguageClient } from 'vscode-languageclient';
 import * as library from './library'
-import * as protocol from './protocol';
+import * as protocol from './protocol'
+import { Content_Provider } from './content_provider'
 
 
-/* Uri information */
+/* HTML content */
 
-const preview_uri_template = Uri.parse("isabelle-preview:")
-const preview_uri_scheme = preview_uri_template.scheme
+const content_provider = new Content_Provider("isabelle-preview")
 
 function encode_preview(document_uri: Uri | undefined): Uri | undefined
 {
   if (document_uri && library.is_file(document_uri)) {
-    return preview_uri_template.with({ query: document_uri.fsPath })
+    return content_provider.uri_template.with({ query: document_uri.fsPath })
   }
   else undefined
 }
 
 function decode_preview(preview_uri: Uri | undefined): Uri | undefined
 {
-  if (preview_uri && preview_uri.scheme === preview_uri_scheme) {
+  if (preview_uri && preview_uri.scheme === content_provider.uri_scheme) {
     return Uri.file(preview_uri.query)
   }
   else undefined
 }
 
 
-/* HTML content */
-
-const preview_content = new Map<string, string>()
-
-class Content_Provider implements TextDocumentContentProvider
-{
-  dispose() { }
-
-  private emitter = new EventEmitter<Uri>()
-  public update(preview_uri: Uri) { this.emitter.fire(preview_uri) }
-  get onDidChange(): Event<Uri> { return this.emitter.event }
-
-  provideTextDocumentContent(preview_uri: Uri): string
-  {
-    return preview_content.get(preview_uri.toString()) || ""
-  }
-}
-
-
-/* init */
+/* setup */
 
 let language_client: LanguageClient
-let content_provider: Content_Provider
-
-export function init(context: ExtensionContext, client: LanguageClient)
-{
-  language_client = client
 
-  content_provider = new Content_Provider()
-  context.subscriptions.push(
-    workspace.registerTextDocumentContentProvider(preview_uri_scheme, content_provider),
-    content_provider)
+export function setup(context: ExtensionContext, client: LanguageClient)
+{
+  context.subscriptions.push(content_provider.register())
 
+  language_client = client
   language_client.onNotification(protocol.preview_response_type, params =>
     {
       const preview_uri = encode_preview(Uri.parse(params.uri))
       if (preview_uri) {
-        preview_content.set(preview_uri.toString(), params.content)
+        content_provider.set_content(preview_uri, params.content)
         content_provider.update(preview_uri)
 
         const existing_document =
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/protocol.ts
--- a/src/Tools/VSCode/extension/src/protocol.ts	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/src/protocol.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -47,6 +47,28 @@
   new NotificationType<Dynamic_Output, void>("PIDE/dynamic_output")
 
 
+/* state */
+
+export interface State_Output
+{
+  id: number
+  content: string
+}
+
+export const state_output_type =
+  new NotificationType<State_Output, void>("PIDE/state_output")
+
+export interface State_Id
+{
+  id: number
+}
+
+export const state_init_type = new NotificationType<void, void>("PIDE/state_init")
+export const state_exit_type = new NotificationType<State_Id, void>("PIDE/state_exit")
+export const state_locate_type = new NotificationType<State_Id, void>("PIDE/state_locate")
+export const state_update_type = new NotificationType<State_Id, void>("PIDE/state_update")
+
+
 /* preview */
 
 export interface Preview_Request
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/extension/src/symbol.ts
--- a/src/Tools/VSCode/extension/src/symbol.ts	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/extension/src/symbol.ts	Sat Jun 17 14:52:23 2017 +0200
@@ -113,7 +113,7 @@
   registerSubstitutions: (substitutions: LanguageEntry) => Disposable
 }
 
-export function init(context: ExtensionContext, entries: [Entry])
+export function setup(context: ExtensionContext, entries: [Entry])
 {
   update_entries(entries)
 
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -48,12 +48,13 @@
       catch { case ERROR(_) => Nil }
   }
 
-  def init(session: Session, node_name: Document.Node.Name): Document_Model =
-    Document_Model(session, node_name, Content.empty)
+  def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
+    Document_Model(session, editor, node_name, Content.empty)
 }
 
 sealed case class Document_Model(
   session: Session,
+  editor: Server.Editor,
   node_name: Document.Node.Name,
   content: Document_Model.Content,
   external_file: Boolean = false,
@@ -109,8 +110,10 @@
             case None => Text.Perspective.empty
           }
 
+      val overlays = editor.node_overlays(node_name)
+
       (snapshot.node.load_commands_changed(doc_blobs),
-        Document.Node.Perspective(node_required, text_perspective, Document.Node.Overlays.empty))
+        Document.Node.Perspective(node_required, text_perspective, overlays))
     }
     else (false, Document.Node.no_perspective_text)
   }
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/preview.scala
--- a/src/Tools/VSCode/src/preview.scala	Thu Jun 15 17:22:23 2017 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,56 +0,0 @@
-/*  Title:      Tools/VSCode/src/preview.scala
-    Author:     Makarius
-
-HTML document preview.
-*/
-
-package isabelle.vscode
-
-
-import isabelle._
-
-import java.io.{File => JFile}
-
-
-class Preview(resources: VSCode_Resources)
-{
-  private val pending = Synchronized(Map.empty[JFile, Int])
-
-  def request(file: JFile, column: Int): Unit =
-    pending.change(map => map + (file -> column))
-
-  def flush(channel: Channel): Boolean =
-  {
-    pending.change_result(map =>
-    {
-      val map1 =
-        (map /: map.iterator)({ case (m, (file, column)) =>
-          resources.get_model(file) match {
-            case Some(model) =>
-              val snapshot = model.snapshot()
-              if (snapshot.is_outdated) m
-              else {
-                val (label, content) = make_preview(model, snapshot)
-                channel.write(Protocol.Preview_Response(file, column, label, content))
-                m - file
-              }
-            case None => m - file
-          }
-        })
-      (map1.nonEmpty, map1)
-    })
-  }
-
-  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
-  {
-    val label = "Preview " + quote(model.node_name.toString)
-    val content =
-      HTML.output_document(
-        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
-        List(
-          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
-          HTML.source(Present.theory_document(snapshot))),
-        css = "")
-    (label, content)
-  }
-}
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/preview_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/preview_panel.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -0,0 +1,56 @@
+/*  Title:      Tools/VSCode/src/preview_panel.scala
+    Author:     Makarius
+
+HTML document preview.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+import java.io.{File => JFile}
+
+
+class Preview_Panel(resources: VSCode_Resources)
+{
+  private val pending = Synchronized(Map.empty[JFile, Int])
+
+  def request(file: JFile, column: Int): Unit =
+    pending.change(map => map + (file -> column))
+
+  def flush(channel: Channel): Boolean =
+  {
+    pending.change_result(map =>
+    {
+      val map1 =
+        (map /: map.iterator)({ case (m, (file, column)) =>
+          resources.get_model(file) match {
+            case Some(model) =>
+              val snapshot = model.snapshot()
+              if (snapshot.is_outdated) m
+              else {
+                val (label, content) = make_preview(model, snapshot)
+                channel.write(Protocol.Preview_Response(file, column, label, content))
+                m - file
+              }
+            case None => m - file
+          }
+        })
+      (map1.nonEmpty, map1)
+    })
+  }
+
+  def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) =
+  {
+    val label = "Preview " + quote(model.node_name.toString)
+    val content =
+      HTML.output_document(
+        List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
+        List(
+          HTML.chapter("Theory " + quote(model.node_name.theory_base_name)),
+          HTML.source(Present.theory_document(snapshot))),
+        css = "")
+    (label, content)
+  }
+}
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/protocol.scala
--- a/src/Tools/VSCode/src/protocol.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/src/protocol.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -462,10 +462,33 @@
 
   object Dynamic_Output
   {
-    def apply(body: String): JSON.T =
-      Notification("PIDE/dynamic_output", Map("content" -> body))
+    def apply(content: String): JSON.T =
+      Notification("PIDE/dynamic_output", Map("content" -> content))
+  }
+
+
+  /* state output */
+
+  object State_Output
+  {
+    def apply(id: Counter.ID, content: String): JSON.T =
+      Notification("PIDE/state_output", Map("id" -> id, "content" -> content))
   }
 
+  class State_Id_Notification(name: String)
+  {
+    def unapply(json: JSON.T): Option[Counter.ID] =
+      json match {
+        case Notification(method, Some(params)) if method == name => JSON.long(params, "id")
+        case _ => None
+      }
+  }
+
+  object State_Init extends Notification0("PIDE/state_init")
+  object State_Exit extends State_Id_Notification("PIDE/state_exit")
+  object State_Locate extends State_Id_Notification("PIDE/state_locate")
+  object State_Update extends State_Id_Notification("PIDE/state_update")
+
 
   /* preview */
 
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -21,6 +21,9 @@
 
 object Server
 {
+  type Editor = isabelle.Editor[Unit]
+
+
   /* Isabelle tool wrapper */
 
   private lazy val default_logic = Isabelle_System.getenv("ISABELLE_LOGIC")
@@ -118,7 +121,8 @@
 
   private val delay_load: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_load_delay"), channel.Error_Logger) {
-      val (invoke_input, invoke_load) = resources.resolve_dependencies(session, file_watcher)
+      val (invoke_input, invoke_load) =
+        resources.resolve_dependencies(session, editor, file_watcher)
       if (invoke_input) delay_input.invoke()
       if (invoke_load) delay_load.invoke
     }
@@ -158,7 +162,7 @@
     }
     norm(changes)
     norm_changes.foreach(change =>
-      resources.change_model(session, file, change.text, change.range))
+      resources.change_model(session, editor, file, change.text, change.range))
 
     delay_input.invoke()
     delay_output.invoke()
@@ -181,17 +185,17 @@
 
   /* preview */
 
-  private lazy val preview = new Preview(resources)
+  private lazy val preview_panel = new Preview_Panel(resources)
 
   private lazy val delay_preview: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_output_delay"), channel.Error_Logger)
     {
-      if (preview.flush(channel)) delay_preview.invoke()
+      if (preview_panel.flush(channel)) delay_preview.invoke()
     }
 
   private def request_preview(file: JFile, column: Int)
   {
-    preview.request(file, column)
+    preview_panel.request(file, column)
     delay_preview.invoke()
   }
 
@@ -400,6 +404,10 @@
           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 Protocol.State_Init(()) => State_Panel.init(server)
+          case Protocol.State_Exit(id) => State_Panel.exit(id)
+          case Protocol.State_Locate(id) => State_Panel.locate(id)
+          case Protocol.State_Update(id) => State_Panel.update(id)
           case Protocol.Preview_Request(file, column) => request_preview(file, column)
           case Protocol.Symbols_Request(()) => channel.write(Protocol.Symbols())
           case _ => log("### IGNORED")
@@ -426,12 +434,17 @@
 
   /* abstract editor operations */
 
-  object editor extends Editor[Unit]
+  object editor extends Server.Editor
   {
+    /* session */
+
     override def session: Session = server.session
     override def flush(): Unit = resources.flush_input(session)
     override def invoke(): Unit = delay_input.invoke()
 
+
+    /* current situation */
+
     override def current_node(context: Unit): Option[Document.Node.Name] =
       resources.get_caret().map(_.model.node_name)
     override def current_node_snapshot(context: Unit): Option[Document.Snapshot] =
@@ -455,8 +468,31 @@
     override def current_command(context: Unit, snapshot: Document.Snapshot): Option[Command] =
       current_command(snapshot)
 
+
+    /* overlays */
+
+    override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+      resources.node_overlays(name)
+
+    override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+      resources.insert_overlay(command, fn, args)
+
+    override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+      resources.remove_overlay(command, fn, args)
+
+
+    /* hyperlinks */
+
     override def hyperlink_command(
       focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0)
         : Option[Hyperlink] = None
+
+
+    /* dispatcher thread */
+
+    override def assert_dispatcher[A](body: => A): A = session.assert_dispatcher(body)
+    override def require_dispatcher[A](body: => A): A = session.require_dispatcher(body)
+    override def send_dispatcher(body: => Unit): Unit = session.send_dispatcher(body)
+    override def send_wait_dispatcher(body: => Unit): Unit = session.send_wait_dispatcher(body)
   }
 }
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/state_panel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/VSCode/src/state_panel.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -0,0 +1,121 @@
+/*  Title:      Tools/VSCode/src/state_panel.scala
+    Author:     Makarius
+
+Show proof state.
+*/
+
+package isabelle.vscode
+
+
+import isabelle._
+
+
+object State_Panel
+{
+  private val make_id = Counter.make()
+  private val instances = Synchronized(Map.empty[Counter.ID, State_Panel])
+
+  def init(server: Server)
+  {
+    val instance = new State_Panel(server)
+    instances.change(_ + (instance.id -> instance))
+    instance.init()
+  }
+
+  def exit(id: Counter.ID)
+  {
+    instances.change(map =>
+      map.get(id) match {
+        case None => map
+        case Some(instance) => instance.exit(); map - id
+      })
+  }
+
+  def locate(id: Counter.ID): Unit =
+    instances.value.get(id).foreach(state =>
+      state.server.editor.send_dispatcher(state.locate()))
+
+  def update(id: Counter.ID): Unit =
+    instances.value.get(id).foreach(state =>
+      state.server.editor.send_dispatcher(state.update()))
+}
+
+
+class State_Panel private(val server: Server)
+{
+  /* output */
+
+  val id: Counter.ID = State_Panel.make_id()
+
+  private def output(content: String): Unit =
+    server.channel.write(Protocol.State_Output(id, content))
+
+
+  /* query operation */
+
+  private val print_state =
+    new Query_Operation(server.editor, (), "print_state", _ => (),
+      (snapshot, results, body) =>
+        {
+          val text = server.resources.output_pretty_message(Pretty.separate(body))
+          val content =
+            HTML.output_document(
+              List(HTML.style(HTML.fonts_css()),
+                HTML.style_file(Url.print_file(HTML.isabelle_css.file))),
+              List(
+                HTML.chapter("Proof state"),
+                HTML.source(text)),
+              css = "")
+          output(content)
+        })
+
+  def locate() { print_state.locate_query() }
+
+  def update()
+  {
+    server.editor.current_node_snapshot(()) match {
+      case Some(snapshot) =>
+        (server.editor.current_command((), snapshot), print_state.get_location) match {
+          case (Some(command1), Some(command2)) if command1.id == command2.id =>
+          case _ => print_state.apply_query(Nil)
+        }
+      case None =>
+    }
+  }
+
+
+  /* auto update */
+
+  private val auto_update_enabled = Synchronized(true)
+
+  def set_auto_update(b: Boolean) { auto_update_enabled.change(_ => b); if (b) update() }
+
+  def auto_update() { if (auto_update_enabled.value) update() }
+
+
+  /* main */
+
+  private val main =
+    Session.Consumer[Any](getClass.getName) {
+      case changed: Session.Commands_Changed =>
+        if (changed.assignment) auto_update()
+
+      case Session.Caret_Focus =>
+        auto_update()
+    }
+
+  def init()
+  {
+    server.session.commands_changed += main
+    server.session.caret_focus += main
+    server.editor.send_wait_dispatcher { print_state.activate() }
+    server.editor.send_dispatcher { auto_update() }
+  }
+
+  def exit()
+  {
+    server.editor.send_wait_dispatcher { print_state.deactivate() }
+    server.session.commands_changed -= main
+    server.session.caret_focus -= main
+  }
+}
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -21,6 +21,7 @@
   sealed case class State(
     models: Map[JFile, Document_Model] = Map.empty,
     caret: Option[(JFile, Line.Position)] = None,
+    overlays: Document.Overlays = Document.Overlays.empty,
     pending_input: Set[JFile] = Set.empty,
     pending_output: Set[JFile] = Set.empty)
   {
@@ -49,6 +50,14 @@
           (_, model) <- models.iterator
           blob <- model.get_blob
         } yield (model.node_name -> blob)).toMap)
+
+    def change_overlay(insert: Boolean, file: JFile,
+        command: Command, fn: String, args: List[String]): State =
+      copy(
+        overlays =
+          if (insert) overlays.insert(command, fn, args)
+          else overlays.remove(command, fn, args),
+        pending_input = pending_input + file)
   }
 
 
@@ -147,11 +156,16 @@
       case None => false
     }
 
-  def change_model(session: Session, file: JFile, text: String, range: Option[Line.Range] = None)
+  def change_model(
+    session: Session,
+    editor: Server.Editor,
+    file: JFile,
+    text: String,
+    range: Option[Line.Range] = None)
   {
     state.change(st =>
       {
-        val model = st.models.getOrElse(file, Document_Model.init(session, node_name(file)))
+        val model = st.models.getOrElse(file, Document_Model.init(session, editor, node_name(file)))
         val model1 = (model.change_text(text, range) getOrElse model).external(false)
         st.update_models(Some(file -> model1))
       })
@@ -178,9 +192,24 @@
       })
 
 
+  /* overlays */
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    state.value.overlays(name)
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(true, node_file(command.node_name), command, fn, args))
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(_.change_overlay(false, node_file(command.node_name), command, fn, args))
+
+
   /* resolve dependencies */
 
-  def resolve_dependencies(session: Session, file_watcher: File_Watcher): (Boolean, Boolean) =
+  def resolve_dependencies(
+    session: Session,
+    editor: Server.Editor,
+    file_watcher: File_Watcher): (Boolean, Boolean) =
   {
     state.change_result(st =>
       {
@@ -217,7 +246,7 @@
             text <- { file_watcher.register_parent(file); read_file_content(file) }
           }
           yield {
-            val model = Document_Model.init(session, node_name)
+            val model = Document_Model.init(session, editor, node_name)
             val model1 = (model.change_text(text) getOrElse model).external(true)
             (file, model1)
           }).toList
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -27,7 +27,8 @@
 
   sealed case class State(
     models: Map[Document.Node.Name, Document_Model] = Map.empty,
-    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty)
+    buffer_models: Map[JEditBuffer, Buffer_Model] = Map.empty,
+    overlays: Document.Overlays = Document.Overlays.empty)
   {
     def file_models_iterator: Iterator[(Document.Node.Name, File_Model)] =
       for {
@@ -83,6 +84,18 @@
     } yield info.map((_, model))
 
 
+  /* overlays */
+
+  def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    state.value.overlays(name)
+
+  def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(st => st.copy(overlays = st.overlays.insert(command, fn, args)))
+
+  def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    state.change(st => st.copy(overlays = st.overlays.remove(command, fn, args)))
+
+
   /* sync external files */
 
   def sync_files(changed_files: Set[JFile]): Boolean =
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/jEdit/src/jedit_editor.scala
--- a/src/Tools/jEdit/src/jedit_editor.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -83,6 +83,18 @@
   }
 
 
+  /* overlays */
+
+  override def node_overlays(name: Document.Node.Name): Document.Node.Overlays =
+    Document_Model.node_overlays(name)
+
+  override def insert_overlay(command: Command, fn: String, args: List[String]): Unit =
+    Document_Model.insert_overlay(command, fn, args)
+
+  override def remove_overlay(command: Command, fn: String, args: List[String]): Unit =
+    Document_Model.remove_overlay(command, fn, args)
+
+
   /* navigation */
 
   def push_position(view: View)
@@ -284,4 +296,12 @@
         hyperlink_command(focus, snapshot, id, range.start)
       case _ => None
     }
+
+
+  /* dispatcher thread */
+
+  override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body)
+  override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body)
+  override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body)
+  override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body)
 }
diff -r def95e0bc529 -r 8ff7fd4ee919 src/Tools/jEdit/src/state_dockable.scala
--- a/src/Tools/jEdit/src/state_dockable.scala	Thu Jun 15 17:22:23 2017 +0100
+++ b/src/Tools/jEdit/src/state_dockable.scala	Sat Jun 17 14:52:23 2017 +0200
@@ -64,7 +64,7 @@
   {
     GUI_Thread.require {}
 
-    Document_Model.get(view.getBuffer).map(_.snapshot()) match {
+    PIDE.editor.current_node_snapshot(view) match {
       case Some(snapshot) =>
         (PIDE.editor.current_command(view, snapshot), print_state.get_location) match {
           case (Some(command1), Some(command2)) if command1.id == command2.id =>