# HG changeset patch
# User wenzelm
# Date 1514498025 -3600
# Node ID 386ddccfccbfe61118084211517a6d14d89a8382
# Parent  1bd9a0142d7a9b35a858408a77b5ca237fc2abdd
implicit thy_load context for bibtex files (VSCode);

diff -r 1bd9a0142d7a -r 386ddccfccbf src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Dec 28 22:36:15 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Dec 28 22:53:45 2017 +0100
@@ -58,7 +58,8 @@
   }
 
   def init(session: Session, editor: Server.Editor, node_name: Document.Node.Name): Document_Model =
-    Document_Model(session, editor, node_name, Content.empty)
+    Document_Model(session, editor, node_name, Content.empty,
+      node_required = Bibtex.is_bibtex_theory(node_name))
 }
 
 sealed case class Document_Model(
diff -r 1bd9a0142d7a -r 386ddccfccbf src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Thu Dec 28 22:36:15 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Thu Dec 28 22:53:45 2017 +0100
@@ -439,6 +439,7 @@
           case Protocol.Exit(()) => exit()
           case Protocol.DidOpenTextDocument(file, _, version, text) =>
             change_document(file, version, List(Protocol.TextDocumentChange(None, text)))
+            delay_load.invoke()
           case Protocol.DidChangeTextDocument(file, version, changes) =>
             change_document(file, version, changes)
           case Protocol.DidCloseTextDocument(file) => close_document(file)
diff -r 1bd9a0142d7a -r 386ddccfccbf src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 28 22:36:15 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Thu Dec 28 22:53:45 2017 +0100
@@ -75,6 +75,8 @@
     log: Logger = No_Logger)
   extends Resources(session_base, log = log)
 {
+  resources =>
+
   private val state = Synchronized(VSCode_Resources.State())
 
 
@@ -96,7 +98,7 @@
       val theory = theory_name(Sessions.DRAFT, Thy_Header.theory_name(node))
       if (session_base.loaded_theory(theory)) Document.Node.Name.loaded_theory(theory)
       else {
-        val master_dir = if (theory == "") "" else file.getParent
+        val master_dir = file.getParent
         Document.Node.Name(node, master_dir, theory)
       }
     }
@@ -120,8 +122,12 @@
   /* file content */
 
   def read_file_content(file: JFile): Option[String] =
-    try { Some(Line.normalize(File.read(file))) }
-    catch { case ERROR(_) => None }
+  {
+    Bibtex.make_theory_content(file) orElse {
+      try { Some(Line.normalize(File.read(file))) }
+      catch { case ERROR(_) => None }
+    }
+  }
 
   def get_file_content(file: JFile): Option[String] =
     get_model(file) match {
@@ -216,7 +222,13 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = dependencies(thys).theories
+        val thy_files1 = resources.dependencies(thys).theories
+
+        val thy_files2 =
+          (for {
+            (_, model) <- st.models.iterator if model.node_name.is_bibtex
+            thy_name <- Bibtex.make_theory_name(resources, model.node_name)
+          } yield thy_name).toList
 
 
         /* auxiliary files */
@@ -237,7 +249,7 @@
 
         val loaded_models =
           (for {
-            node_name <- thy_files.iterator ++ aux_files.iterator
+            node_name <- thy_files1.iterator ++ thy_files2.iterator ++ aux_files.iterator
             file = node_file(node_name)
             if !st.models.isDefinedAt(file)
             text <- { file_watcher.register_parent(file); read_file_content(file) }