1.1 --- a/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:18:04 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:31:56 2016 +0100
     1.3 @@ -94,7 +94,7 @@
     1.4    modes: List[String] = Nil,
     1.5    log: Logger = No_Logger)
     1.6  {
     1.7 -  /* server session */
     1.8 +  /* prover session */
     1.9  
    1.10    private val session_ = Synchronized(None: Option[Session])
    1.11    def session: Session = session_.value getOrElse error("Server inactive")
    1.12 @@ -108,7 +108,16 @@
    1.13      } yield (rendering, offset)
    1.14  
    1.15  
    1.16 -  /* document content */
    1.17 +  /* input from client or file-system */
    1.18 +
    1.19 +  private val delay_input =
    1.20 +    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    1.21 +    { resources.flush_input(session) }
    1.22 +
    1.23 +  private val watcher = File_Watcher(sync_documents(_))
    1.24 +
    1.25 +  private def sync_documents(changed: Set[JFile]): Unit =
    1.26 +    if (resources.sync_models(changed)) delay_input.invoke()
    1.27  
    1.28    private def update_document(uri: String, text: String)
    1.29    {
    1.30 @@ -121,34 +130,14 @@
    1.31      resources.close_model(uri) match {
    1.32        case Some(model) =>
    1.33          model.register(watcher)
    1.34 -        sync_external(Set(model.file))
    1.35 +        sync_documents(Set(model.file))
    1.36        case None =>
    1.37      }
    1.38    }
    1.39  
    1.40 -  private def sync_external(changed: Set[JFile]): Unit =
    1.41 -    if (resources.sync_models(changed)) delay_input.invoke()
    1.42 -
    1.43 -  private val watcher = File_Watcher(sync_external(_))
    1.44 -
    1.45 -
    1.46 -  /* input from client */
    1.47 -
    1.48 -  private val delay_input =
    1.49 -    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    1.50 -    { resources.flush_input(session) }
    1.51 -
    1.52  
    1.53    /* output to client */
    1.54  
    1.55 -  private val commands_changed =
    1.56 -    Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.57 -      case changed if changed.nodes.nonEmpty =>
    1.58 -        resources.update_output(changed.nodes.toList.map(_.node))
    1.59 -        delay_output.invoke()
    1.60 -      case _ =>
    1.61 -    }
    1.62 -
    1.63    private val delay_output: Standard_Thread.Delay =
    1.64      Standard_Thread.delay_last(options.seconds("vscode_output_delay"))
    1.65      {
    1.66 @@ -156,13 +145,15 @@
    1.67        else resources.flush_output(channel)
    1.68      }
    1.69  
    1.70 -
    1.71 -  /* file watcher */
    1.72 -
    1.73 +  private val prover_output =
    1.74 +    Session.Consumer[Session.Commands_Changed](getClass.getName) {
    1.75 +      case changed if changed.nodes.nonEmpty =>
    1.76 +        resources.update_output(changed.nodes.toList.map(_.node))
    1.77 +        delay_output.invoke()
    1.78 +      case _ =>
    1.79 +    }
    1.80  
    1.81 -  /* syslog */
    1.82 -
    1.83 -  private val all_messages =
    1.84 +  private val syslog =
    1.85      Session.Consumer[Prover.Message](getClass.getName) {
    1.86        case output: Prover.Output if output.is_syslog =>
    1.87          channel.log_writeln(XML.content(output.message))
    1.88 @@ -213,8 +204,8 @@
    1.89          }
    1.90        session.phase_changed += session_phase
    1.91  
    1.92 -      session.commands_changed += commands_changed
    1.93 -      session.all_messages += all_messages
    1.94 +      session.commands_changed += prover_output
    1.95 +      session.all_messages += syslog
    1.96  
    1.97        session.start(receiver =>
    1.98          Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
    1.99 @@ -235,8 +226,8 @@
   1.100            Session.Consumer(getClass.getName) {
   1.101              case Session.Inactive =>
   1.102                session.phase_changed -= session_phase
   1.103 -              session.commands_changed -= commands_changed
   1.104 -              session.all_messages -= all_messages
   1.105 +              session.commands_changed -= prover_output
   1.106 +              session.all_messages -= syslog
   1.107                reply("")
   1.108              case _ =>
   1.109            }