# HG changeset patch
# User wenzelm
# Date 1513892517 -3600
# Node ID 68177abb29885015204701906f431334cb51d47b
# Parent  3a965131801526263ef7ad3424149f7176766d42
isabelle.preview presents bibtex database files as well;

diff -r 3a9651318015 -r 68177abb2988 NEWS
--- a/NEWS	Thu Dec 21 22:38:28 2017 +0100
+++ b/NEWS	Thu Dec 21 22:41:57 2017 +0100
@@ -70,7 +70,8 @@
 "isabelle.antiquoted_cartouche" turns an antiquotation with 0 or 1
 arguments into this format.
 
-* Action "isabelle.preview" presents auxiliary text files as well.
+* Action "isabelle.preview" is able to present more file formats,
+notably bibtex database files and plain text files.
 
 
 
diff -r 3a9651318015 -r 68177abb2988 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Thu Dec 21 22:38:28 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Thu Dec 21 22:41:57 2017 +0100
@@ -503,6 +503,7 @@
       "unsortlist" -> "html-u")
 
   def html_output(bib: List[Path],
+    body: Boolean = false,
     citations: List[String] = List("*"),
     style: String = "empty",
     chronological: Boolean = false): String =
@@ -553,10 +554,21 @@
 
       val html = File.read(tmp_dir + out_file)
 
-      cat_lines(
-        split_lines(html).
-          dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
-          dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
+      if (body) {
+        cat_lines(
+          split_lines(html).
+            dropWhile(line => !line.startsWith("<!-- BEGIN BIBLIOGRAPHY")).reverse.
+            dropWhile(line => !line.startsWith("<!-- END BIBLIOGRAPHY")).reverse)
+      }
+      else html
     })
   }
+
+  def present(snapshot: Document.Snapshot): String =
+  {
+    Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+      File.write(bib, snapshot.node.get_text)
+      html_output(List(bib), style = "unsortlist")
+    }
+  }
 }
diff -r 3a9651318015 -r 68177abb2988 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:38:28 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Dec 21 22:41:57 2017 +0100
@@ -329,16 +329,19 @@
   {
     val snapshot = await_stable_snapshot()
 
-    HTML.output_document(
-      List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
-        css = "",
-        body =
-          if (is_theory)
-            List(HTML.chapter("Theory " + quote(node_name.theory_base_name)),
-              HTML.source(Present.theory_document(snapshot)))
-          else
-            List(HTML.chapter("File " + quote(node_name.node)),
-              HTML.source(Present.text_document(snapshot))))
+    if (is_bibtex) Bibtex.present(snapshot)
+    else {
+      HTML.output_document(
+        List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css))),
+          css = "",
+          body =
+            if (is_theory)
+              List(HTML.chapter("Theory " + quote(node_name.theory_base_name)),
+                HTML.source(Present.theory_document(snapshot)))
+            else
+              List(HTML.chapter("File " + quote(node_name.node)),
+                HTML.source(Present.text_document(snapshot))))
+    }
   }
 
 
@@ -558,7 +561,7 @@
 
   def bibtex_entries: List[Text.Info[String]] =
     GUI_Thread.require {
-      if (Bibtex.check_name(node_name)) {
+      if (node_name.is_bibtex) {
         _bibtex_entries match {
           case Some(entries) => entries
           case None =>