# 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 _ => }