# HG changeset patch
# User wenzelm
# Date 1513955448 -3600
# Node ID ce7d856680d1b74ce49f733ba637214615285487
# Parent  f1f9834848784a36e3aeb8fc1d4ceb2a66770cda
proper title;
clarified modules;

diff -r f1f983484878 -r ce7d856680d1 src/Pure/Thy/present.scala
--- a/src/Pure/Thy/present.scala	Fri Dec 22 15:49:44 2017 +0100
+++ b/src/Pure/Thy/present.scala	Fri Dec 22 16:10:48 2017 +0100
@@ -108,17 +108,23 @@
     require(!snapshot.is_outdated)
 
     val name = snapshot.node_name
-    if (name.is_bibtex && !plain) Bibtex.present(snapshot)
+    if (name.is_bibtex && !plain) {
+      val title = "Bibliography " + quote(name.path.base_name)
+      Isabelle_System.with_tmp_file("bib", "bib") { bib =>
+        File.write(bib, snapshot.node.source)
+        Bibtex.html_output(List(bib), style = "unsort", title = title)
+      }
+    }
     else {
-      val (heading, body) =
+      val (title, body) =
         if (name.is_theory && !plain)
           ("Theory " + quote(name.theory_base_name), pide_document(snapshot))
         else ("File " + quote(name.path.base_name), text_document(snapshot))
 
       HTML.output_document(
         List(HTML.style(HTML.fonts_css(HTML.fonts_dir(fonts_dir)) + File.read(HTML.isabelle_css)),
-          HTML.title(heading)),
-          List(HTML.chapter(heading), HTML.source(body)))
+          HTML.title(title)),
+          List(HTML.chapter(title), HTML.source(body)))
     }
   }
 
diff -r f1f983484878 -r ce7d856680d1 src/Pure/Tools/bibtex.scala
--- a/src/Pure/Tools/bibtex.scala	Fri Dec 22 15:49:44 2017 +0100
+++ b/src/Pure/Tools/bibtex.scala	Fri Dec 22 16:10:48 2017 +0100
@@ -503,6 +503,7 @@
       "unsortlist" -> "html-u")
 
   def html_output(bib: List[Path],
+    title: String = "Bibliography",
     body: Boolean = false,
     citations: List[String] = List("*"),
     style: String = "empty",
@@ -548,8 +549,9 @@
 
       Isabelle_System.bash(
         "\"$BIB2XHTML_HOME/main/bib2xhtml.pl\" -B \"$ISABELLE_BIBTEX\"" +
-          " -u -s " + Bash.string(style) + (if (chronological) " -c " else " ") +
-          File.bash_path(in_file) + " " + File.bash_path(out_file),
+          " -u -s " + Bash.string(style) + (if (chronological) " -c" else "") +
+          (if (title != "") " -h " + Bash.string(title) + " " else "") +
+          " " + File.bash_path(in_file) + " " + File.bash_path(out_file),
         cwd = tmp_dir.file).check
 
       val html = File.read(tmp_dir + out_file)
@@ -563,12 +565,4 @@
       else html
     })
   }
-
-  def present(snapshot: Document.Snapshot): String =
-  {
-    Isabelle_System.with_tmp_file("bib", "bib") { bib =>
-      File.write(bib, snapshot.node.source)
-      html_output(List(bib), style = "unsort")
-    }
-  }
 }