# HG changeset patch
# User wenzelm
# Date 1483212394 -3600
# Node ID 13e37567a0d6c339f2fcc61aa9955b1d680c3510
# Parent  c534a2ac537d4256250eaeed5778f3b00ef1b65f
automatically resolve dependencies from document models and file-system;

diff -r c534a2ac537d -r 13e37567a0d6 src/Tools/VSCode/etc/options
--- a/src/Tools/VSCode/etc/options	Sat Dec 31 15:32:54 2016 +0100
+++ b/src/Tools/VSCode/etc/options	Sat Dec 31 20:26:34 2016 +0100
@@ -6,6 +6,9 @@
 option vscode_output_delay : real = 0.5
   -- "delay for client output (rendering)"
 
+option vscode_load_delay : real = 0.5
+  -- "delay for file load operations"
+
 option vscode_tooltip_margin : int = 60
   -- "margin for pretty-printing of tooltips"
 
diff -r c534a2ac537d -r 13e37567a0d6 src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Sat Dec 31 15:32:54 2016 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sat Dec 31 20:26:34 2016 +0100
@@ -47,6 +47,8 @@
 
   val file: JFile = VSCode_Resources.canonical_file(uri)
 
+  def external(b: Boolean): Document_Model = copy(external_file = b)
+
   def register(watcher: File_Watcher)
   {
     val dir = file.getParentFile
diff -r c534a2ac537d -r 13e37567a0d6 src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Sat Dec 31 15:32:54 2016 +0100
+++ b/src/Tools/VSCode/src/server.scala	Sat Dec 31 20:26:34 2016 +0100
@@ -114,7 +114,12 @@
     Standard_Thread.delay_last(options.seconds("vscode_input_delay"))
     { resources.flush_input(session) }
 
-  private val watcher = File_Watcher(sync_documents(_))
+  private val delay_load =
+    Standard_Thread.delay_last(options.seconds("vscode_load_delay"))
+    { if (resources.resolve_dependencies(session)) delay_input.invoke() }
+
+  private val watcher =
+    File_Watcher(sync_documents(_), options.seconds("vscode_load_delay"))
 
   private def sync_documents(changed: Set[JFile]): Unit =
     if (resources.sync_models(changed)) delay_input.invoke()
@@ -178,7 +183,10 @@
         val content = Build.session_content(options, false, session_dirs, session_name)
         val resources =
           new VSCode_Resources(options, text_length, content.loaded_theories,
-            content.known_theories, content.syntax, log)
+              content.known_theories, content.syntax, log) {
+            override def commit(change: Session.Change): Unit =
+              if (change.deps_changed) delay_load.invoke()
+          }
 
         Some(new Session(resources) {
           override def output_delay = options.seconds("editor_output_delay")
diff -r c534a2ac537d -r 13e37567a0d6 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 15:32:54 2016 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Dec 31 20:26:34 2016 +0100
@@ -12,6 +12,8 @@
 import java.net.{URI, URISyntaxException}
 import java.io.{File => JFile}
 
+import scala.util.parsing.input.{Reader, CharSequenceReader}
+
 
 object VSCode_Resources
 {
@@ -64,6 +66,23 @@
     else name.copy(node = "file://" + name.node)
   }
 
+  override def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
+  {
+    val uri = name.node
+    get_model(uri) match {
+      case Some(model) =>
+        val reader = new CharSequenceReader(model.doc.make_text)
+        f(reader)
+
+      case None =>
+        val file = VSCode_Resources.canonical_file(uri)
+        if (!file.isFile) error("No such file: " + quote(file.toString))
+
+        val reader = Scan.byte_reader(file)
+        try { f(reader) } finally { reader.close }
+    }
+  }
+
 
   /* document models */
 
@@ -74,7 +93,7 @@
     state.change(st =>
       {
         val model = st.models.getOrElse(uri, Document_Model.init(session, uri))
-        val model1 = (model.update_text(text) getOrElse model).copy(external_file = false)
+        val model1 = (model.update_text(text) getOrElse model).external(false)
         st.copy(
           models = st.models + (uri -> model1),
           pending_input = st.pending_input + uri)
@@ -86,7 +105,7 @@
       st.models.get(uri) match {
         case None => (None, st)
         case Some(model) =>
-          (Some(model), st.copy(models = st.models + (uri -> model.copy(external_file = true))))
+          (Some(model), st.copy(models = st.models + (uri -> model.external(true))))
       })
 
   def sync_models(changed_files: Set[JFile]): Boolean =
@@ -106,6 +125,40 @@
       })
 
 
+  /* resolve dependencies */
+
+  def resolve_dependencies(session: Session): Boolean =
+  {
+    val thys =
+      (for ((_, model) <- state.value.models.iterator if model.is_theory)
+       yield (model.node_name, Position.none)).toList
+    val deps = new Thy_Info(this).dependencies("", thys).deps
+
+    state.change_result(st =>
+      {
+        val loaded_models =
+          for {
+            uri <- deps.map(_.name.node)
+            if get_model(uri).isEmpty
+            text <-
+              try { Some(File.read(VSCode_Resources.canonical_file(uri))) }
+              catch { case ERROR(_) => None }
+          }
+          yield {
+            val model = Document_Model.init(session, uri)
+            val model1 = (model.update_text(text) getOrElse model).external(true)
+            (uri, model1)
+          }
+        if (loaded_models.isEmpty) (false, st)
+        else
+          (true,
+            st.copy(
+              models = st.models ++ loaded_models,
+              pending_input = st.pending_input ++ loaded_models.map(_._1)))
+      })
+  }
+
+
   /* pending input */
 
   def flush_input(session: Session)