# HG changeset patch
# User wenzelm
# Date 1483126573 -3600
# Node ID 72ca4e5f976e7bd9218251e2176a352c7bafc023
# Parent  5e6566ab78bf48999fd58f5d06622fc0e4ad73db
manage changes of external files;
tuned;

diff -r 5e6566ab78bf -r 72ca4e5f976e src/Pure/General/file_watcher.scala
--- a/src/Pure/General/file_watcher.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Pure/General/file_watcher.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -99,7 +99,7 @@
 
   /* shutdown */
 
-  def shutdown
+  def shutdown()
   {
     watcher_thread.interrupt
     watcher_thread.join
diff -r 5e6566ab78bf -r 72ca4e5f976e src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -9,6 +9,8 @@
 
 import isabelle._
 
+import java.io.{File => JFile}
+
 import scala.util.parsing.input.CharSequenceReader
 
 
@@ -23,10 +25,11 @@
   }
 }
 
-sealed case class Document_Model private(
+sealed case class Document_Model(
   session: Session,
   node_name: Document.Node.Name,
   doc: Line.Document,
+  external: Boolean = false,
   node_visible: Boolean = true,
   node_required: Boolean = false,
   last_perspective: Document.Node.Perspective_Text = Document.Node.no_perspective_text,
@@ -41,6 +44,17 @@
   def is_theory: Boolean = node_name.is_theory
 
 
+  /* external file */
+
+  val file: JFile = VSCode_Resources.canonical_file(uri)
+
+  def register(watcher: File_Watcher)
+  {
+    val dir = file.getParentFile
+    if (dir != null && dir.isDirectory) watcher.register(dir)
+  }
+
+
   /* header */
 
   def node_header: Document.Node.Header =
@@ -64,19 +78,26 @@
 
   /* edits */
 
-  def update_text(new_text: String): Document_Model =
+  def update_text(new_text: String): Option[Document_Model] =
   {
     val old_text = doc.make_text
-    if (new_text == old_text) this
+    if (new_text == old_text) None
     else {
       val doc1 = Line.Document(new_text, doc.text_length)
       val pending_edits1 =
         if (old_text != "") pending_edits :+ Text.Edit.remove(0, old_text) else pending_edits
       val pending_edits2 = pending_edits1 :+ Text.Edit.insert(0, new_text)
-      copy(doc = doc1, pending_edits = pending_edits2)
+      Some(copy(doc = doc1, pending_edits = pending_edits2))
     }
   }
 
+  def update_file: Option[Document_Model] =
+    if (external) {
+      try { update_text(File.read(file)) }
+      catch { case ERROR(_) => None }
+    }
+    else None
+
   def flush_edits: Option[(List[Document.Edit_Text], Document_Model)] =
   {
     val perspective = node_perspective
diff -r 5e6566ab78bf -r 72ca4e5f976e src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -11,7 +11,7 @@
 
 import isabelle._
 
-import java.io.{PrintStream, OutputStream}
+import java.io.{PrintStream, OutputStream, File => JFile}
 
 import scala.annotation.tailrec
 
@@ -106,11 +106,7 @@
     } yield (rendering, offset)
 
 
-  /* input from client */
-
-  private val delay_input =
-    Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
-    { resources.flush_input(session) }
+  /* document content */
 
   private def update_document(uri: String, text: String)
   {
@@ -118,6 +114,28 @@
     delay_input.invoke()
   }
 
+  private def close_document(uri: String)
+  {
+    resources.close_model(uri) match {
+      case Some(model) =>
+        model.register(watcher)
+        sync_external(Set(model.file))
+      case None =>
+    }
+  }
+
+  private def sync_external(changed: Set[JFile]): Unit =
+    if (resources.sync_external(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 */
 
@@ -137,6 +155,9 @@
     }
 
 
+  /* file watcher */
+
+
   /* syslog */
 
   private val all_messages =
@@ -221,6 +242,7 @@
         session.stop()
         delay_input.revoke()
         delay_output.revoke()
+        watcher.shutdown()
         None
       case None =>
         reply("Prover inactive")
@@ -280,7 +302,8 @@
             update_document(uri, text)
           case Protocol.DidChangeTextDocument(uri, version, List(Protocol.TextDocumentContent(text))) =>
             update_document(uri, text)
-          case Protocol.DidCloseTextDocument(uri) => channel.log("CLOSE " + uri)
+          case Protocol.DidCloseTextDocument(uri) =>
+            close_document(uri)
           case Protocol.DidSaveTextDocument(uri) => channel.log("SAVE " + uri)
           case Protocol.Hover(id, node_pos) => hover(id, node_pos)
           case Protocol.GotoDefinition(id, node_pos) => goto_definition(id, node_pos)
diff -r 5e6566ab78bf -r 72ca4e5f976e src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 17:45:00 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Dec 30 20:36:13 2016 +0100
@@ -64,13 +64,35 @@
   {
     state.change(st =>
       {
-        val model = st.models.getOrElse(uri, Document_Model.init(session, uri)).update_text(text)
+        val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
+        val model1 = (model.update_text(text) getOrElse model).copy(external = false)
         st.copy(
-          models = st.models + (uri -> model),
+          models = st.models + (uri -> model1),
           pending_input = st.pending_input + uri)
       })
   }
 
+  def close_model(uri: String): Option[Document_Model] =
+    state.change_result(st =>
+      st.models.get(uri) match {
+        case None => (None, st)
+        case Some(model) =>
+          (Some(model), st.copy(models = st.models + (uri -> model.copy(external = true))))
+      })
+
+  def sync_external(changed_files: Set[JFile]): Boolean =
+    state.change_result(st =>
+      {
+        val changed =
+          (for {
+            (uri, model) <- st.models.iterator
+            if changed_files(model.file)
+            model1 <- model.update_file
+          } yield (uri, model)).toList
+        if (changed.isEmpty) (false, st)
+        else (true, st.copy(models = (st.models /: changed)(_ + _)))
+      })
+
 
   /* pending input */