# HG changeset patch # User wenzelm # Date 1605710201 -3600 # Node ID 4ba5b1b08dd5d8f5e7029e3fdb872de8c6f99695 # Parent 1cbac4ae934d388e2dbe98aa9759e8022a0d0278 clarified signature: more explicit types; diff -r 1cbac4ae934d -r 4ba5b1b08dd5 src/Pure/Thy/present.scala --- a/src/Pure/Thy/present.scala Wed Nov 18 13:16:08 2020 +0100 +++ b/src/Pure/Thy/present.scala Wed Nov 18 15:36:41 2020 +0100 @@ -12,6 +12,34 @@ object Present { + /* document variants */ + + object Document_Variant + { + def parse(s: String): Document_Variant = + Library.space_explode('=', s) match { + case List(name) => Document_Variant(name) + case List(name, tags) => Document_Variant(name, Library.space_explode(',', tags)) + case _ => error("Malformed document variant: " + quote(s)) + } + } + + sealed case class Document_Variant(name: String, tags: List[String] = Nil) + { + def print: String = if (tags.isEmpty) name else name + "=" + tags.mkString(",") + def path: Path = Path.basic(name) + def latex_sty: String = + Library.terminate_lines( + tags.map(tag => + tag.toList match { + case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" + case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" + case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" + case cs => "\\isakeeptag{" + cs.mkString + "}" + })) + } + + /* presentation context */ object Context @@ -141,8 +169,8 @@ else Nil val document_links = - for ((name, _) <- info.documents) - yield HTML.link(Path.basic(name).pdf, HTML.text(name)) + for (doc <- info.documents) + yield HTML.link(doc.path.pdf, HTML.text(doc.name)) Library.separate(HTML.break ::: HTML.nl, (deps_link :: readme_links ::: document_links). @@ -271,16 +299,6 @@ def tex_name(name: Document.Node.Name): String = name.theory_base_name + ".tex" def document_tex_name(name: Document.Node.Name): String = "document/" + tex_name(name) - def isabelletags(tags: List[String]): String = - Library.terminate_lines( - tags.map(tag => - tag.toList match { - case '/' :: cs => "\\isafoldtag{" + cs.mkString + "}" - case '-' :: cs => "\\isadroptag{" + cs.mkString + "}" - case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}" - case cs => "\\isakeeptag{" + cs.mkString + "}" - })) - def build_documents( session: String, deps: Sessions.Deps, @@ -288,7 +306,7 @@ progress: Progress = new Progress, presentation: Context = Context.none, verbose: Boolean = false, - verbose_latex: Boolean = false): List[(String, Bytes)] = + verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] = { /* session info */ @@ -309,13 +327,13 @@ } ) - def prepare_dir(dir: Path, doc_name: String, doc_tags: List[String]): (Path, String) = + def prepare_dir(dir: Path, doc: Document_Variant): (Path, String) = { - val doc_dir = dir + Path.basic(doc_name) + val doc_dir = dir + Path.basic(doc.name) Isabelle_System.make_directory(doc_dir) Isabelle_System.bash("isabelle latex -o sty", cwd = doc_dir.file).check - File.write(doc_dir + Path.explode("isabelletags.sty"), isabelletags(doc_tags)) + File.write(doc_dir + Path.explode("isabelletags.sty"), doc.latex_sty) for ((base_dir, src) <- info.document_files) File.copy_base(info.dir + base_dir, src, doc_dir) Bytes.write(doc_dir + session_graph_path, graph_pdf) @@ -325,7 +343,7 @@ for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) - val root1 = "root_" + doc_name + val root1 = "root_" + doc.name val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" (doc_dir, root) @@ -336,13 +354,13 @@ val doc_output = info.document_output - val docs = - for ((doc_name, doc_tags) <- info.documents) + val documents = + for (doc <- info.documents) yield { Isabelle_System.with_tmp_dir("document")(tmp_dir => { - val (doc_dir, root) = prepare_dir(tmp_dir, doc_name, doc_tags) - doc_output.foreach(prepare_dir(_, doc_name, doc_tags)) + val (doc_dir, root) = prepare_dir(tmp_dir, doc) + doc_output.foreach(prepare_dir(_, doc)) // bash scripts @@ -361,7 +379,7 @@ val result = if ((doc_dir + Path.explode("build")).is_file) { - bash("./build pdf " + Bash.string(doc_name)) + bash("./build pdf " + Bash.string(doc.name)) } else { bash( @@ -382,20 +400,20 @@ cat_error( Library.trim_line(result.err), cat_lines(Latex.latex_errors(doc_dir, root) ::: Bibtex.bibtex_errors(doc_dir, root)), - "Failed to build document " + quote(doc_name)) + "Failed to build document " + quote(doc.name)) } else if (!result_path.is_file) { error("Bad document result: expected to find " + root_pdf) } - else doc_name -> Bytes.read(result_path) + else doc -> Bytes.read(result_path) }) } def output(dir: Path) { Isabelle_System.make_directory(dir) - for ((name, pdf) <- docs) { - val path = dir + Path.basic(name).pdf + for ((doc, pdf) <- documents) { + val path = dir + doc.path.pdf Bytes.write(path, pdf) progress.echo_document(path) } @@ -407,7 +425,7 @@ doc_output.foreach(output) - docs + documents } diff -r 1cbac4ae934d -r 4ba5b1b08dd5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Nov 18 13:16:08 2020 +0100 +++ b/src/Pure/Thy/sessions.scala Wed Nov 18 15:36:41 2020 +0100 @@ -492,20 +492,21 @@ case doc => error("Bad document specification " + quote(doc)) } - def documents: List[(String, List[String])] = + def documents_variants: List[Present.Document_Variant] = { val variants = - for (s <- Library.space_explode(':', options.string("document_variants"))) - yield { - Library.space_explode('=', s) match { - case List(name) => (name, Nil) - case List(name, tags) => (name, Library.space_explode(',', tags)) - case _ => error("Malformed document_variants: " + quote(s)) - } - } - val dups = Library.duplicates(variants.map(_._1)) + Library.space_explode(':', options.string("document_variants")). + map(Present.Document_Variant.parse) + + val dups = Library.duplicates(variants.map(_.name)) if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups)) + variants + } + + def documents: List[Present.Document_Variant] = + { + val variants = documents_variants if (!document_enabled || document_files.isEmpty) Nil else variants }