--- 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)))
}
}
--- 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")
- }
- }
}