src/Tools/VSCode/src/server.scala
changeset 64710 72ca4e5f976e
parent 64709 5e6566ab78bf
child 64717 d2b50eb3d9ab
     1.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 17:45:00 2016 +0100
     1.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 20:36:13 2016 +0100
     1.3 @@ -11,7 +11,7 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import java.io.{PrintStream, OutputStream}
     1.8 +import java.io.{PrintStream, OutputStream, File => JFile}
     1.9  
    1.10  import scala.annotation.tailrec
    1.11  
    1.12 @@ -106,11 +106,7 @@
    1.13      } yield (rendering, offset)
    1.14  
    1.15  
    1.16 -  /* input from client */
    1.17 -
    1.18 -  private val delay_input =
    1.19 -    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    1.20 -    { resources.flush_input(session) }
    1.21 +  /* document content */
    1.22  
    1.23    private def update_document(uri: String, text: String)
    1.24    {
    1.25 @@ -118,6 +114,28 @@
    1.26      delay_input.invoke()
    1.27    }
    1.28  
    1.29 +  private def close_document(uri: String)
    1.30 +  {
    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 +      case None =>
    1.36 +    }
    1.37 +  }
    1.38 +
    1.39 +  private def sync_external(changed: Set[JFile]): Unit =
    1.40 +    if (resources.sync_external(changed)) delay_input.invoke()
    1.41 +
    1.42 +  private val watcher = File_Watcher(sync_external(_))
    1.43 +
    1.44 +
    1.45 +  /* input from client */
    1.46 +
    1.47 +  private val delay_input =
    1.48 +    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    1.49 +    { resources.flush_input(session) }
    1.50 +
    1.51  
    1.52    /* output to client */
    1.53  
    1.54 @@ -137,6 +155,9 @@
    1.55      }
    1.56  
    1.57  
    1.58 +  /* file watcher */
    1.59 +
    1.60 +
    1.61    /* syslog */
    1.62  
    1.63    private val all_messages =
    1.64 @@ -221,6 +242,7 @@
    1.65          session.stop()
    1.66          delay_input.revoke()
    1.67          delay_output.revoke()
    1.68 +        watcher.shutdown()
    1.69          None
    1.70        case None =>
    1.71          reply("Prover inactive")
    1.72 @@ -280,7 +302,8 @@
    1.73              update_document(uri, text)
    1.74            case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
    1.75              update_document(uri, text)
    1.76 -          case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
    1.77 +          case Protocol.DidCloseTextDocument(uri) =>
    1.78 +            close_document(uri)
    1.79            case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
    1.80            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    1.81            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)