tuned;
authorwenzelm
Sat Dec 31 15:31:56 2016 +0100 (2016-12-31)
changeset 6472538305f56c769
parent 64724 44dbf8cc2d7f
child 64726 c534a2ac537d
tuned;
src/Tools/VSCode/src/document_model.scala
src/Tools/VSCode/src/server.scala
     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            }