1.1 --- a/src/Pure/General/file_watcher.scala	Fri Dec 30 17:45:00 2016 +0100
     1.2 +++ b/src/Pure/General/file_watcher.scala	Fri Dec 30 20:36:13 2016 +0100
     1.3 @@ -99,7 +99,7 @@
     1.4  
     1.5    /* shutdown */
     1.6  
     1.7 -  def shutdown
     1.8 +  def shutdown()
     1.9    {
    1.10      watcher_thread.interrupt
    1.11      watcher_thread.join

     2.1 --- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 17:45:00 2016 +0100
     2.2 +++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 20:36:13 2016 +0100
     2.3 @@ -9,6 +9,8 @@
     2.4  
     2.5  import isabelle._
     2.6  
     2.7 +import java.io.{File => JFile}
     2.8 +
     2.9  import scala.util.parsing.input.CharSequenceReader
    2.10  
    2.11  
    2.12 @@ -23,10 +25,11 @@
    2.13    }
    2.14  }
    2.15  
    2.16 -sealed case class Document_Model private(
    2.17 +sealed case class Document_Model(
    2.18    session: Session,
    2.19    node_name: Document.Node.Name,
    2.20    doc: Line.Document,
    2.21 +  external: Boolean = false,
    2.22    node_visible: Boolean = true,
    2.23    node_required: Boolean = false,
    2.24    last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
    2.25 @@ -41,6 +44,17 @@
    2.26    def is_theory: Boolean = node_name.is_theory
    2.27  
    2.28  
    2.29 +  /* external file */
    2.30 +
    2.31 +  val file: JFile = VSCode_Resources.canonical_file(uri)
    2.32 +
    2.33 +  def register(watcher: File_Watcher)
    2.34 +  {
    2.35 +    val dir = file.getParentFile
    2.36 +    if (dir != null && dir.isDirectory) watcher.register(dir)
    2.37 +  }
    2.38 +
    2.39 +
    2.40    /* header */
    2.41  
    2.42    def node_header: Document.Node.Header =
    2.43 @@ -64,19 +78,26 @@
    2.44  
    2.45    /* edits */
    2.46  
    2.47 -  def update_text(new_text: String): Document_Model =
    2.48 +  def update_text(new_text: String): Option[Document_Model] =
    2.49    {
    2.50      val old_text = doc.make_text
    2.51 -    if (new_text == old_text) this
    2.52 +    if (new_text == old_text) None
    2.53      else {
    2.54        val doc1 = Line.Document(new_text, doc.text_length)
    2.55        val pending_edits1 =
    2.56          if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits
    2.57        val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text)
    2.58 -      copy(doc = doc1, pending_edits = pending_edits2)
    2.59 +      Some(copy(doc = doc1, pending_edits = pending_edits2))
    2.60      }
    2.61    }
    2.62  
    2.63 +  def update_file: Option[Document_Model] =
    2.64 +    if (external) {
    2.65 +      try { update_text(File.read(file)) }
    2.66 +      catch { case ERROR(_) => None }
    2.67 +    }
    2.68 +    else None
    2.69 +
    2.70    def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
    2.71    {
    2.72      val perspective = node_perspective

     3.1 --- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 17:45:00 2016 +0100
     3.2 +++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 20:36:13 2016 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  import isabelle._
     3.6  
     3.7 -import java.io.{PrintStream, OutputStream}
     3.8 +import java.io.{PrintStream, OutputStream, File => JFile}
     3.9  
    3.10  import scala.annotation.tailrec
    3.11  
    3.12 @@ -106,11 +106,7 @@
    3.13      } yield (rendering, offset)
    3.14  
    3.15  
    3.16 -  /* input from client */
    3.17 -
    3.18 -  private val delay_input =
    3.19 -    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    3.20 -    { resources.flush_input(session) }
    3.21 +  /* document content */
    3.22  
    3.23    private def update_document(uri: String, text: String)
    3.24    {
    3.25 @@ -118,6 +114,28 @@
    3.26      delay_input.invoke()
    3.27    }
    3.28  
    3.29 +  private def close_document(uri: String)
    3.30 +  {
    3.31 +    resources.close_model(uri) match {
    3.32 +      case Some(model) =>
    3.33 +        model.register(watcher)
    3.34 +        sync_external(Set(model.file))
    3.35 +      case None =>
    3.36 +    }
    3.37 +  }
    3.38 +
    3.39 +  private def sync_external(changed: Set[JFile]): Unit =
    3.40 +    if (resources.sync_external(changed)) delay_input.invoke()
    3.41 +
    3.42 +  private val watcher = File_Watcher(sync_external(_))
    3.43 +
    3.44 +
    3.45 +  /* input from client */
    3.46 +
    3.47 +  private val delay_input =
    3.48 +    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
    3.49 +    { resources.flush_input(session) }
    3.50 +
    3.51  
    3.52    /* output to client */
    3.53  
    3.54 @@ -137,6 +155,9 @@
    3.55      }
    3.56  
    3.57  
    3.58 +  /* file watcher */
    3.59 +
    3.60 +
    3.61    /* syslog */
    3.62  
    3.63    private val all_messages =
    3.64 @@ -221,6 +242,7 @@
    3.65          session.stop()
    3.66          delay_input.revoke()
    3.67          delay_output.revoke()
    3.68 +        watcher.shutdown()
    3.69          None
    3.70        case None =>
    3.71          reply("Prover inactive")
    3.72 @@ -280,7 +302,8 @@
    3.73              update_document(uri, text)
    3.74            case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
    3.75              update_document(uri, text)
    3.76 -          case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
    3.77 +          case Protocol.DidCloseTextDocument(uri) =>
    3.78 +            close_document(uri)
    3.79            case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
    3.80            case Protocol.Hover(id, node_pos) => hover(id, node_pos)
    3.81            case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)

     4.1 --- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 17:45:00 2016 +0100
     4.2 +++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 20:36:13 2016 +0100
     4.3 @@ -64,13 +64,35 @@
     4.4    {
     4.5      state.change(st =>
     4.6        {
     4.7 -        val model = st.models.getOrElse(uri, Document_Model.init(session, uri)).update_text(text)
     4.8 +        val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
     4.9 +        val model1 = (model.update_text(text) getOrElse model).copy(external = false)
    4.10          st.copy(
    4.11 -          models = st.models + (uri -> model),
    4.12 +          models = st.models + (uri -> model1),
    4.13            pending_input = st.pending_input + uri)
    4.14        })
    4.15    }
    4.16  
    4.17 +  def close_model(uri: String): Option[Document_Model] =
    4.18 +    state.change_result(st =>
    4.19 +      st.models.get(uri) match {
    4.20 +        case None => (None, st)
    4.21 +        case Some(model) =>
    4.22 +          (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
    4.23 +      })
    4.24 +
    4.25 +  def sync_external(changed_files: Set[JFile]): Boolean =
    4.26 +    state.change_result(st =>
    4.27 +      {
    4.28 +        val changed =
    4.29 +          (for {
    4.30 +            (uri, model) <- st.models.iterator
    4.31 +            if changed_files(model.file)
    4.32 +            model1 <- model.update_file
    4.33 +          } yield (uri, model)).toList
    4.34 +        if (changed.isEmpty) (false, st)
    4.35 +        else (true, st.copy(models = (st.models /: changed)(_ + _)))
    4.36 +      })
    4.37 +
    4.38  
    4.39    /* pending input */
    4.40