# HG changeset patch
# User wenzelm
# Date 1483194716 -3600
# Node ID 38305f56c769afd3a717529f57690d3eb67fef9d
# Parent  44dbf8cc2d7f92703a30e8eb1b5567b0e9a3efc0
tuned;

diff -r 44dbf8cc2d7f -r 38305f56c769 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Dec 31 15:18:04 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Dec 31 15:31:56 2016 +0100
@@ -127,7 +127,7 @@
   }
 
 
-  /* session */
+  /* prover session */
 
   def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
 
diff -r 44dbf8cc2d7f -r 38305f56c769 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:18:04 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:31:56 2016 +0100
@@ -94,7 +94,7 @@
   modes: List[String] = Nil,
   log: Logger = No_Logger)
 {
-  /* server session */
+  /* prover session */
 
   private val session_ = Synchronized(None: Option[Session])
   def session: Session = session_.value getOrElse error("Server inactive")
@@ -108,7 +108,16 @@
     } yield (rendering, offset)
 
 
-  /* document content */
+  /* input from client or file-system */
+
+  private val delay_input =
+    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
+    { resources.flush_input(session) }
+
+  private val watcher = File_Watcher(sync_documents(_))
+
+  private def sync_documents(changed: Set[JFile]): Unit =
+    if (resources.sync_models(changed)) delay_input.invoke()
 
   private def update_document(uri: String, text: String)
   {
@@ -121,34 +130,14 @@
     resources.close_model(uri) match {
       case Some(model) =>
         model.register(watcher)
-        sync_external(Set(model.file))
+        sync_documents(Set(model.file))
       case None =>
     }
   }
 
-  private def sync_external(changed: Set[JFile]): Unit =
-    if (resources.sync_models(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 */
 
-  private val commands_changed =
-    Session.Consumer[Session.Commands_Changed](getClass.getName) {
-      case changed if changed.nodes.nonEmpty =>
-        resources.update_output(changed.nodes.toList.map(_.node))
-        delay_output.invoke()
-      case _ =>
-    }
-
   private val delay_output: Standard_Thread.Delay =
     Standard_Thread.delay_last(options.seconds("vscode_output_delay"))
     {
@@ -156,13 +145,15 @@
       else resources.flush_output(channel)
     }
 
-
-  /* file watcher */
-
+  private val prover_output =
+    Session.Consumer[Session.Commands_Changed](getClass.getName) {
+      case changed if changed.nodes.nonEmpty =>
+        resources.update_output(changed.nodes.toList.map(_.node))
+        delay_output.invoke()
+      case _ =>
+    }
 
-  /* syslog */
-
-  private val all_messages =
+  private val syslog =
     Session.Consumer[Prover.Message](getClass.getName) {
       case output: Prover.Output if output.is_syslog =>
         channel.log_writeln(XML.content(output.message))
@@ -213,8 +204,8 @@
         }
       session.phase_changed += session_phase
 
-      session.commands_changed += commands_changed
-      session.all_messages += all_messages
+      session.commands_changed += prover_output
+      session.all_messages += syslog
 
       session.start(receiver =>
         Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
@@ -235,8 +226,8 @@
           Session.Consumer(getClass.getName) {
             case Session.Inactive =>
               session.phase_changed -= session_phase
-              session.commands_changed -= commands_changed
-              session.all_messages -= all_messages
+              session.commands_changed -= prover_output
+              session.all_messages -= syslog
               reply("")
             case _ =>
           }