# HG changeset patch
# User wenzelm
# Date 1514493928 -3600
# Node ID 98b6cd12f9633f521ad7dcce137e837a69dd29ed
# Parent  bef14fa789ef569098021cd970296b5f4b30ca58
implicit thy_load context for bibtex files;

diff -r bef14fa789ef -r 98b6cd12f963 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -119,7 +119,7 @@
 
       def path: Path = Path.explode(File.standard_path(node))
 
-      def is_bibtex: Boolean = Bibtex.check_name(node)
+      def is_bibtex: Boolean = Bibtex.is_bibtex(node)
 
       def is_theory: Boolean = theory.nonEmpty
 
diff -r bef14fa789ef -r 98b6cd12f963 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -189,7 +189,7 @@
   }
 
   def is_hidden(name: Document.Node.Name): Boolean =
-    !name.is_theory || name.theory == Sessions.root_name
+    !name.is_theory || name.theory == Sessions.root_name || Bibtex.is_bibtex_theory(name)
 
 
   /* blobs */
diff -r bef14fa789ef -r 98b6cd12f963 src/Pure/Thy/bibtex.scala
--- a/src/Pure/Thy/bibtex.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/bibtex.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -7,6 +7,8 @@
 package isabelle
 
 
+import java.io.{File => JFile}
+
 import scala.collection.mutable
 import scala.util.parsing.combinator.RegexParsers
 import scala.util.parsing.input.Reader
@@ -129,7 +131,39 @@
 
   /** document model **/
 
-  def check_name(name: String): Boolean = name.endsWith(".bib")
+  /* bibtex files */
+
+  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
+  def is_bibtex_theory(name: Document.Node.Name): Boolean = is_bibtex(name.theory)
+
+  private val node_suffix: String = "bibtex_file"
+
+  def make_theory_name(resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
+  {
+    Thy_Header.file_name(name.node) match {
+      case Some(bib_name) if is_bibtex(bib_name) =>
+        val thy_node = resources.append(name.node, Path.explode(node_suffix))
+        Some(Document.Node.Name(thy_node, name.master_dir, bib_name))
+      case _ => None
+    }
+  }
+
+  def make_theory_content(bib_name: String): Option[String] =
+    if (is_bibtex(bib_name)) {
+      Some("""theory "bib" imports Pure begin bibtex_file """ + quote(bib_name) + """ end""")
+    }
+    else None
+
+  def make_theory_content(file: JFile): Option[String] =
+    if (file.getName == node_suffix) {
+      val parent = file.getParentFile
+      if (parent != null && is_bibtex(parent.getName)) make_theory_content(parent.getName)
+      else None
+    }
+    else None
+
+
+  /* entries */
 
   def entries(text: String): List[Text.Info[String]] =
   {
diff -r bef14fa789ef -r 98b6cd12f963 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -30,7 +30,7 @@
   def exclude_session(name: String): Boolean = name == "" || name == DRAFT
 
   def exclude_theory(name: String): Boolean =
-    name == root_name || name == "README" || name == "index"
+    name == root_name || name == "README" || name == "index" || name == "bib"
 
 
   /* base info and source dependencies */
diff -r bef14fa789ef -r 98b6cd12f963 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -85,6 +85,12 @@
   def is_base_name(s: String): Boolean =
     s != "" && !s.exists("/\\:".contains(_))
 
+  def file_name(s: String): Option[String] =
+    s match {
+      case File_Name(s) => Some(s)
+      case _ => None
+    }
+
   def import_name(s: String): String =
     s match {
       case File_Name(name) if !name.endsWith(".thy") => name
diff -r bef14fa789ef -r 98b6cd12f963 src/Tools/jEdit/src/jedit_bibtex.scala
--- a/src/Tools/jEdit/src/jedit_bibtex.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_bibtex.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -35,7 +35,7 @@
       case text_area: TextArea =>
         text_area.getBuffer match {
           case buffer: Buffer
-          if (Bibtex.check_name(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
+          if (Bibtex.is_bibtex(JEdit_Lib.buffer_name(buffer)) && buffer.isEditable) =>
             val menu = new JMenu("BibTeX entries")
             for (entry <- Bibtex.known_entries) {
               val item = new JMenuItem(entry.kind)
diff -r bef14fa789ef -r 98b6cd12f963 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -46,7 +46,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 vfs.getParentOfPath(path)
+        val master_dir = vfs.getParentOfPath(path)
         Document.Node.Name(node, master_dir, theory)
       }
     }
@@ -80,14 +80,16 @@
 
   def read_file_content(node_name: Document.Node.Name): Option[String] =
   {
-    val name = node_name.node
-    try {
-      val text =
-        if (Url.is_wellformed(name)) Url.read(Url(name))
-        else File.read(new JFile(name))
-      Some(Symbol.decode(Line.normalize(text)))
+    Bibtex.make_theory_content(node_name.theory) orElse {
+      val name = node_name.node
+      try {
+        val text =
+          if (Url.is_wellformed(name)) Url.read(Url(name))
+          else File.read(new JFile(name))
+        Some(Symbol.decode(Line.normalize(text)))
+      }
+      catch { case ERROR(_) => None }
     }
-    catch { case ERROR(_) => None }
   }
 
   def get_file_content(node_name: Document.Node.Name): Option[String] =
diff -r bef14fa789ef -r 98b6cd12f963 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -126,7 +126,13 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.dependencies(thys).theories
+          val thy_files1 = resources.dependencies(thys).theories
+
+          val thy_files2 =
+            (for {
+              (name, _) <- models.iterator if name.is_bibtex
+              thy_name <- Bibtex.make_theory_name(resources, name)
+            } yield thy_name).toList
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {
@@ -141,7 +147,7 @@
             }
             else Nil
 
-          (thy_files ::: aux_files).filterNot(models.isDefinedAt(_))
+          (thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt(_))
         }
         if (required_files.nonEmpty) {
           try {