src/Tools/VSCode/src/vscode_resources.scala
changeset 67292 386ddccfccbf
parent 67104 a2fa0c6a7aff
child 67547 aefe7a7b330a
--- 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) }