src/Tools/VSCode/src/server.scala

--- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -11,7 +11,7 @@
 
 import isabelle._
 
-import java.io.{PrintStream, OutputStream}
+import java.io.{PrintStream, OutputStream, File => JFile}
 
 import scala.annotation.tailrec
 
@@ -106,11 +106,7 @@
     } yield (rendering, offset)
 
 
-  /* input from client */
-
-  private val delay_input =
-    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
-    { resources.flush_input(session) }
+  /* document content */
 
   private def update_document(uri: String, text: String)
   {
@@ -118,6 +114,28 @@
     delay_input.invoke()
   }
 
+  private def close_document(uri: String)
+  {
+    resources.close_model(uri) match {
+      case Some(model) =>
+        model.register(watcher)
+        sync_external(Set(model.file))
+      case None =>
+    }
+  }
+
+  private def sync_external(changed: Set[JFile]): Unit =
+    if (resources.sync_external(changed)) delay_input.invoke()
+
+  private val watcher = File_Watcher(sync_external(_))
+
+
+  /* input from client */
+
+  private val delay_input =
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
+    { resources.flush_input(session) }
+
 
   /* output to client */
 
@@ -137,6 +155,9 @@
     }
 
 
+  /* file watcher */
+
+
   /* syslog */
 
   private val all_messages =
@@ -221,6 +242,7 @@
         session.stop()
         delay_input.revoke()
         delay_output.revoke()
+        watcher.shutdown()
         None
       case None =>
         reply("Prover inactive")
@@ -280,7 +302,8 @@
             update_document(uri, text)
           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
             update_document(uri, text)
-          case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
+          case Protocol.DidCloseTextDocument(uri) =>
+            close_document(uri)
           case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)