--- 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]] =