src/Pure/Tools/bibtex.scala
changeset 67248 68177abb2988
parent 67243 6a93aaa3ed36
child 67250 6c837185aa61
--- 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")
+    }
+  }
 }