src/Tools/VSCode/src/server.scala

 package isabelle.vscode
 
 
 import isabelle._
 
-import java.io.{PrintStream, OutputStream}
+import java.io.{PrintStream, OutputStream, File => JFile}
 
 import scala.annotation.tailrec
 
 
 object Server

       rendering = model.rendering()
       offset <- model.doc.offset(node_pos.pos)
     } yield (rendering, offset)
 
 
+  /* document content */
+
+  private def update_document(uri: String, text: String)
+  {
+    resources.update_model(session, uri, text)
+    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) }
-
-  private def update_document(uri: String, text: String)
-  {
-    resources.update_model(session, uri, text)
-    delay_input.invoke()
-  }
 
 
   /* output to client */
 
   private val commands_changed =

     Standard_Thread.delay_last(options.seconds("vscode_output_delay"))
     {
       if (session.current_state().stable_tip_version.isEmpty) delay_output.invoke()
       else resources.flush_output(channel)
     }
+
+
+  /* file watcher */
 
 
   /* syslog */
 
   private val all_messages =

           }
         session.phase_changed += session_phase
         session.stop()
         delay_input.revoke()
         delay_output.revoke()
+        watcher.shutdown()
         None
       case None =>
         reply("Prover inactive")
         None
     })

           case Protocol.Exit(()) => exit()
           case Protocol.DidOpenTextDocument(uri, lang, version, text) =>
             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)
           case _ => channel.log("### IGNORED")
         }