# HG changeset patch # User wenzelm # Date 1513870143 -3600 # Node ID 6a93aaa3ed3666567dcb77caba828c9a09686129 # Parent 759d4fb30bfcdf71c46c8da16772bd0c63631131 bibtex HTML output via external tool; diff -r 759d4fb30bfc -r 6a93aaa3ed36 Admin/components/components.sha1 --- a/Admin/components/components.sha1 Thu Dec 21 12:19:24 2017 +0100 +++ b/Admin/components/components.sha1 Thu Dec 21 16:29:03 2017 +0100 @@ -3,6 +3,7 @@ 81250148f8b89ac3587908fb20645081d7f53207 bash_process-1.2.1.tar.gz 97b2491382130a841b3bbaebdcf8720c4d4fb227 bash_process-1.2.2.tar.gz 9e21f447bfa0431ae5097301d553dd6df3c58218 bash_process-1.2.tar.gz +a65ce644b6094d41e9f991ef851cf05eff5dd0a9 bib2xhtml-20171221.tar.gz e7ffe4238b61a3c1ee87aca4421e7a612e09b836 ci-extras-1.tar.gz 70105fd6fbfd1a868383fc510772b95234325d31 csdp-6.x.tar.gz 2f6417b8e96a0e4e8354fe0f1a253c18fb55d9a7 cvc3-2.4.1.tar.gz diff -r 759d4fb30bfc -r 6a93aaa3ed36 Admin/components/main --- a/Admin/components/main Thu Dec 21 12:19:24 2017 +0100 +++ b/Admin/components/main Thu Dec 21 16:29:03 2017 +0100 @@ -1,5 +1,6 @@ #main components for everyday use, without big impact on overall build time bash_process-1.2.2 +bib2xhtml-20171221 csdp-6.x cvc4-1.5-3 e-2.0-1 diff -r 759d4fb30bfc -r 6a93aaa3ed36 src/Pure/Tools/bibtex.scala --- a/src/Pure/Tools/bibtex.scala Thu Dec 21 12:19:24 2017 +0100 +++ b/src/Pure/Tools/bibtex.scala Thu Dec 21 16:29:03 2017 +0100 @@ -487,4 +487,76 @@ } (chunks.toList, ctxt) } + + + + /** HTML output **/ + + private val output_styles = + List( + "empty" -> "html-n", + "plain" -> "html-n", + "alpha" -> "html-a", + "named" -> "html-n", + "paragraph" -> "html-n", + "unsort" -> "html-u", + "unsortlist" -> "html-u") + + def html_output(bib: List[Path], + citations: List[String] = List("*"), + style: String = "empty", + chronological: Boolean = false): String = + { + Isabelle_System.with_tmp_dir("bibtex")(tmp_dir => + { + /* database files */ + + val bib_files = bib.map(path => path.split_ext._1) + val bib_names = + { + val names0 = bib_files.map(_.base_name) + if (Library.duplicates(names0).isEmpty) names0 + else names0.zipWithIndex.map({ case (name, i) => (i + 1).toString + "-" + name }) + } + + for ((a, b) <- bib_files zip bib_names) { + File.copy(a.ext("bib"), tmp_dir + Path.basic(b).ext("bib")) + } + + + /* style file */ + + val bst = + output_styles.toMap.get(style) match { + case Some(base) => base + (if (chronological) "c" else "") + ".bst" + case None => + error("Bad style for bibtex HTML output: " + quote(style) + + "\n(expected: " + commas_quote(output_styles.map(_._1)) + ")") + } + File.copy(Path.explode("$BIB2XHTML_HOME/bst") + Path.explode(bst), tmp_dir) + + + /* result */ + + val in_file = Path.explode("bib.aux") + val out_file = Path.explode("bib.html") + + File.write(tmp_dir + in_file, + bib_names.mkString("\\bibdata{", ",", "}\n") + + citations.map(cite => "\\citation{" + cite + "}\n").mkString) + + 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), + cwd = tmp_dir.file).check + + val html = File.read(tmp_dir + out_file) + + cat_lines( + split_lines(html). + dropWhile(line => !line.startsWith("