src/Pure/Thy/bibtex.scala

--- a/src/Pure/Thy/bibtex.scala	Wed Nov 07 14:06:43 2018 +0100
+++ b/src/Pure/Thy/bibtex.scala	Wed Nov 07 21:42:16 2018 +0100
@@ -16,6 +16,54 @@
 
 object Bibtex
 {
+  /** file format **/
+
+  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
+
+  class File_Format extends isabelle.File_Format
+  {
+    val format_name: String = "bibtex"
+    val node_suffix: String = "bibtex_file"
+
+    def detect(name: String): Boolean = is_bibtex(name)
+
+    override def make_theory_name(
+      resources: Resources, name: Document.Node.Name): Option[Document.Node.Name] =
+    {
+      for { (_, ext_name) <- Thy_Header.split_file_name(name.node) if detect(ext_name) }
+      yield {
+        val thy_node = resources.append(name.node, Path.explode(node_suffix))
+        Document.Node.Name(thy_node, name.master_dir, ext_name)
+      }
+    }
+
+    override def make_theory_content(
+      resources: Resources, thy_name: Document.Node.Name): Option[String] =
+    {
+      for {
+        (prefix, suffix) <- Thy_Header.split_file_name(thy_name.node) if suffix == node_suffix
+        (_, ext_name) <- Thy_Header.split_file_name(prefix) if detect(ext_name)
+      } yield """theory "bib" imports Pure begin bibtex_file """ + quote(ext_name) + """ end"""
+    }
+
+    override def make_preview(snapshot: Document.Snapshot): Option[Present.Preview] =
+    {
+      val name = snapshot.node_name
+      if (detect(name.node)) {
+        val title = "Bibliography " + quote(snapshot.node_name.path.base_name)
+        val content =
+          Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+            File.write(bib, snapshot.node.source)
+            Bibtex.html_output(List(bib), style = "unsort", title = title)
+          }
+        Some(Present.Preview(title, content))
+      }
+      else None
+    }
+  }
+
+
+
   /** bibtex errors **/
 
   def bibtex_errors(dir: Path, root_name: String): List[String] =
@@ -122,37 +170,6 @@
 
   /** document model **/
 
-  /* bibtex files */
-
-  def is_bibtex(name: String): Boolean = name.endsWith(".bib")
-
-  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]] =