1.1 --- a/src/Tools/VSCode/src/document_model.scala Sat Dec 31 15:18:04 2016 +0100
1.2 +++ b/src/Tools/VSCode/src/document_model.scala Sat Dec 31 15:31:56 2016 +0100
1.3 @@ -127,7 +127,7 @@
1.4 }
1.5
1.6
1.7 - /* session */
1.8 + /* prover session */
1.9
1.10 def resources: VSCode_Resources = session.resources.asInstanceOf[VSCode_Resources]
1.11
2.1 --- a/src/Tools/VSCode/src/server.scala Sat Dec 31 15:18:04 2016 +0100
2.2 +++ b/src/Tools/VSCode/src/server.scala Sat Dec 31 15:31:56 2016 +0100
2.3 @@ -94,7 +94,7 @@
2.4 modes: List[String] = Nil,
2.5 log: Logger = No_Logger)
2.6 {
2.7 - /* server session */
2.8 + /* prover session */
2.9
2.10 private val session_ = Synchronized(None: Option[Session])
2.11 def session: Session = session_.value getOrElse error("Server inactive")
2.12 @@ -108,7 +108,16 @@
2.13 } yield (rendering, offset)
2.14
2.15
2.16 - /* document content */
2.17 + /* input from client or file-system */
2.18 +
2.19 + private val delay_input =
2.20 + Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
2.21 + { resources.flush_input(session) }
2.22 +
2.23 + private val watcher = File_Watcher(sync_documents(_))
2.24 +
2.25 + private def sync_documents(changed: Set[JFile]): Unit =
2.26 + if (resources.sync_models(changed)) delay_input.invoke()
2.27
2.28 private def update_document(uri: String, text: String)
2.29 {
2.30 @@ -121,34 +130,14 @@
2.31 resources.close_model(uri) match {
2.32 case Some(model) =>
2.33 model.register(watcher)
2.34 - sync_external(Set(model.file))
2.35 + sync_documents(Set(model.file))
2.36 case None =>
2.37 }
2.38 }
2.39
2.40 - private def sync_external(changed: Set[JFile]): Unit =
2.41 - if (resources.sync_models(changed)) delay_input.invoke()
2.42 -
2.43 - private val watcher = File_Watcher(sync_external(_))
2.44 -
2.45 -
2.46 - /* input from client */
2.47 -
2.48 - private val delay_input =
2.49 - Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
2.50 - { resources.flush_input(session) }
2.51 -
2.52
2.53 /* output to client */
2.54
2.55 - private val commands_changed =
2.56 - Session.Consumer[Session.Commands_Changed](getClass.getName) {
2.57 - case changed if changed.nodes.nonEmpty =>
2.58 - resources.update_output(changed.nodes.toList.map(_.node))
2.59 - delay_output.invoke()
2.60 - case _ =>
2.61 - }
2.62 -
2.63 private val delay_output: Standard_Thread.Delay =
2.64 Standard_Thread.delay_last(options.seconds("vscode_output_delay"))
2.65 {
2.66 @@ -156,13 +145,15 @@
2.67 else resources.flush_output(channel)
2.68 }
2.69
2.70 -
2.71 - /* file watcher */
2.72 -
2.73 + private val prover_output =
2.74 + Session.Consumer[Session.Commands_Changed](getClass.getName) {
2.75 + case changed if changed.nodes.nonEmpty =>
2.76 + resources.update_output(changed.nodes.toList.map(_.node))
2.77 + delay_output.invoke()
2.78 + case _ =>
2.79 + }
2.80
2.81 - /* syslog */
2.82 -
2.83 - private val all_messages =
2.84 + private val syslog =
2.85 Session.Consumer[Prover.Message](getClass.getName) {
2.86 case output: Prover.Output if output.is_syslog =>
2.87 channel.log_writeln(XML.content(output.message))
2.88 @@ -213,8 +204,8 @@
2.89 }
2.90 session.phase_changed += session_phase
2.91
2.92 - session.commands_changed += commands_changed
2.93 - session.all_messages += all_messages
2.94 + session.commands_changed += prover_output
2.95 + session.all_messages += syslog
2.96
2.97 session.start(receiver =>
2.98 Isabelle_Process(options = options, logic = session_name, dirs = session_dirs,
2.99 @@ -235,8 +226,8 @@
2.100 Session.Consumer(getClass.getName) {
2.101 case Session.Inactive =>
2.102 session.phase_changed -= session_phase
2.103 - session.commands_changed -= commands_changed
2.104 - session.all_messages -= all_messages
2.105 + session.commands_changed -= prover_output
2.106 + session.all_messages -= syslog
2.107 reply("")
2.108 case _ =>
2.109 }