# HG changeset patch # User wenzelm # Date 1621260925 -7200 # Node ID ecb31c3bf980971dc04ca15d98e9058d258978d0 # Parent 2f4cb9cb087ff887649115a030f6d6d16be16512 clarified modules; diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Admin/build_doc.scala --- a/src/Pure/Admin/build_doc.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/Admin/build_doc.scala Mon May 17 16:15:25 2021 +0200 @@ -55,7 +55,7 @@ progress.echo("Documentation " + quote(doc) + " ...") using(store.open_database_context())(db_context => - Presentation.build_documents(session, deps, db_context, + Document_Build.build_documents(session, deps, db_context, output_pdf = Some(Path.explode("~~/doc")))) None } diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/System/isabelle_tool.scala --- a/src/Pure/System/isabelle_tool.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/System/isabelle_tool.scala Mon May 17 16:15:25 2021 +0200 @@ -187,6 +187,7 @@ Build_Docker.isabelle_tool, Build_Job.isabelle_tool, Doc.isabelle_tool, + Document_Build.isabelle_tool, Dump.isabelle_tool, Export.isabelle_tool, ML_Process.isabelle_tool, @@ -198,7 +199,6 @@ Phabricator.isabelle_tool2, Phabricator.isabelle_tool3, Phabricator.isabelle_tool4, - Presentation.isabelle_tool, Profiling_Report.isabelle_tool, Server.isabelle_tool, Sessions.isabelle_tool, diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Thy/document_build.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Thy/document_build.scala Mon May 17 16:15:25 2021 +0200 @@ -0,0 +1,378 @@ +/* Title: Pure/Thy/document_build.scala + Author: Makarius + +Build theory document (PDF) from session database. +*/ + +package isabelle + + +object Document_Build +{ + /* document variants */ + + abstract class Document_Name + { + def name: String + def path: Path = Path.basic(name) + + override def toString: String = name + } + + object Document_Variant + { + def parse(name: String, tags: String): Document_Variant = + Document_Variant(name, Library.space_explode(',', tags)) + + def parse(opt: String): Document_Variant = + Library.space_explode('=', opt) match { + case List(name) => Document_Variant(name, Nil) + case List(name, tags) => parse(name, tags) + case _ => error("Malformed document variant: " + quote(opt)) + } + } + + sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name + { + def print_tags: String = tags.mkString(",") + def print: String = if (tags.isEmpty) name else name + "=" + print_tags + + 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 + "}" + })) + } + + sealed case class Document_Input(name: String, sources: SHA1.Digest) + extends Document_Name + + sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) + extends Document_Name + { + def log: String = log_xz.uncompress().text + def log_lines: List[String] = split_lines(log) + + def write(db: SQL.Database, session_name: String): Unit = + write_document(db, session_name, this) + } + + + /* SQL data model */ + + object Data + { + val session_name = SQL.Column.string("session_name").make_primary_key + val name = SQL.Column.string("name").make_primary_key + val sources = SQL.Column.string("sources") + val log_xz = SQL.Column.bytes("log_xz") + val pdf = SQL.Column.bytes("pdf") + + val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) + + def where_equal(session_name: String, name: String = ""): SQL.Source = + "WHERE " + Data.session_name.equal(session_name) + + (if (name == "") "" else " AND " + Data.name.equal(name)) + } + + def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = + { + val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) + db.using_statement(select)(stmt => + stmt.execute_query().iterator(res => + { + val name = res.string(Data.name) + val sources = res.string(Data.sources) + Document_Input(name, SHA1.fake(sources)) + }).toList) + } + + def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = + { + val select = Data.table.select(sql = Data.where_equal(session_name, name)) + db.using_statement(select)(stmt => + { + val res = stmt.execute_query() + if (res.next()) { + val name = res.string(Data.name) + val sources = res.string(Data.sources) + val log_xz = res.bytes(Data.log_xz) + val pdf = res.bytes(Data.pdf) + Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) + } + else None + }) + } + + def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = + { + db.using_statement(Data.table.insert())(stmt => + { + stmt.string(1) = session_name + stmt.string(2) = doc.name + stmt.string(3) = doc.sources.toString + stmt.bytes(4) = doc.log_xz + stmt.bytes(5) = doc.pdf + stmt.execute() + }) + } + + + + /* build documents */ + + val session_tex_path = Path.explode("session.tex") + + 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) + + class Build_Error(val log_lines: List[String], val message: String) + extends Exn.User_Error(message) + + def build_documents( + session: String, + deps: Sessions.Deps, + db_context: Sessions.Database_Context, + progress: Progress = new Progress, + output_sources: Option[Path] = None, + output_pdf: Option[Path] = None, + verbose: Boolean = false, + verbose_latex: Boolean = false): List[Document_Output] = + { + /* session info */ + + val info = deps.sessions_structure(session) + val hierarchy = deps.sessions_structure.hierarchy(session) + val options = info.options + val base = deps(session) + val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) + + + /* prepare document directory */ + + lazy val tex_files = + for (name <- base.session_theories ::: base.document_theories) + yield { + val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name)) + Path.basic(tex_name(name)) -> entry.uncompressed + } + + def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = + { + 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"), doc.latex_sty) + for ((base_dir, src) <- info.document_files) { + Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) + } + + File.write(doc_dir + session_tex_path, + Library.terminate_lines( + base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) + + for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) + + val root1 = "root_" + doc.name + val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" + + (doc_dir, root) + } + + def prepare_dir2(dir: Path, doc: Document_Variant): Unit = + { + val doc_dir = dir + Path.basic(doc.name) + + // non-deterministic, but irrelevant + Bytes.write(doc_dir + Presentation.session_graph_path, graph_pdf) + } + + + /* produce documents */ + + val documents = + for (doc <- info.documents) + yield { + Isabelle_System.with_tmp_dir("document")(tmp_dir => + { + progress.echo("Preparing " + session + "/" + doc.name + " ...") + val start = Time.now() + + + // prepare sources + + val (doc_dir, root) = prepare_dir1(tmp_dir, doc) + val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) + val sources = SHA1.digest_set(digests) + prepare_dir2(tmp_dir, doc) + + for (dir <- output_sources) { + prepare_dir1(dir, doc) + prepare_dir2(dir, doc) + } + + + // old document from database + + val old_document = + for { + old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) + if old_doc.sources == sources + } + yield { + Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) + old_doc + } + + old_document getOrElse { + // bash scripts + + def root_bash(ext: String): String = Bash.string(root + "." + ext) + + def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = + "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) + + def bash(items: String*): Process_Result = + progress.bash(items.mkString(" && "), cwd = doc_dir.file, + echo = verbose_latex, watchdog = Time.seconds(0.5)) + + + // prepare document + + val result = + if ((doc_dir + Path.explode("build")).is_file) { + bash("./build pdf " + Bash.string(doc.name)) + } + else { + bash( + latex_bash(), + "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", + "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", + latex_bash(), + latex_bash()) + } + + + // result + + val root_pdf = Path.basic(root).pdf + val result_path = doc_dir + root_pdf + + val log_lines = result.out_lines ::: result.err_lines + + val errors = + (if (result.ok) Nil else List(result.err)) ::: + Latex.latex_errors(doc_dir, root) ::: + Bibtex.bibtex_errors(doc_dir, root) + + if (errors.nonEmpty) { + val message = + Exn.cat_message( + (errors ::: List("Failed to build document " + quote(doc.name))):_*) + throw new Build_Error(log_lines, message) + } + else if (!result_path.is_file) { + val message = "Bad document result: expected to find " + root_pdf + throw new Build_Error(log_lines, message) + } + else { + val stop = Time.now() + val timing = stop - start + progress.echo("Finished " + session + "/" + doc.name + + " (" + timing.message_hms + " elapsed time)") + + val log_xz = Bytes(cat_lines(log_lines)).compress() + val pdf = Bytes.read(result_path) + Document_Output(doc.name, sources, log_xz, pdf) + } + } + }) + } + + for (dir <- output_pdf; doc <- documents) { + Isabelle_System.make_directory(dir) + val path = dir + doc.path.pdf + Bytes.write(path, doc.pdf) + progress.echo("Document at " + path.absolute) + } + + documents + } + + + /* Isabelle tool wrapper */ + + val isabelle_tool = + Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => + { + var output_sources: Option[Path] = None + var output_pdf: Option[Path] = None + var verbose_latex = false + var dirs: List[Path] = Nil + var options = Options.init() + var verbose_build = false + + val getopts = Getopts( + """ +Usage: isabelle document [OPTIONS] SESSION + + Options are: + -O DIR output directory for LaTeX sources and resulting PDF + -P DIR output directory for resulting PDF + -S DIR output directory for LaTeX sources + -V verbose latex + -d DIR include session directory + -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) + -v verbose build + + Prepare the theory document of a session. +""", + "O:" -> (arg => + { + val dir = Path.explode(arg) + output_sources = Some(dir) + output_pdf = Some(dir) + }), + "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), + "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), + "V" -> (_ => verbose_latex = true), + "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), + "o:" -> (arg => options = options + arg), + "v" -> (_ => verbose_build = true)) + + val more_args = getopts(args) + val session = + more_args match { + case List(a) => a + case _ => getopts.usage() + } + + val progress = new Console_Progress(verbose = verbose_build) + val store = Sessions.store(options) + + progress.interrupt_handler { + val res = + Build.build(options, selection = Sessions.Selection.session(session), + dirs = dirs, progress = progress, verbose = verbose_build) + if (!res.ok) error("Failed to build session " + quote(session)) + + val deps = + Sessions.load_structure(options + "document=pdf", dirs = dirs). + selection_deps(Sessions.Selection.session(session)) + + if (output_sources.isEmpty && output_pdf.isEmpty) { + progress.echo_warning("No output directory") + } + + using(store.open_database_context())(db_context => + build_documents(session, deps, db_context, progress = progress, + output_sources = output_sources, output_pdf = output_pdf, + verbose = true, verbose_latex = verbose_latex)) + } + }) +} diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Thy/presentation.scala --- a/src/Pure/Thy/presentation.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/Thy/presentation.scala Mon May 17 16:15:25 2021 +0200 @@ -1,7 +1,7 @@ -/* Title: Pure/Thy/present.scala +/* Title: Pure/Thy/presentation.scala Author: Makarius -HTML/PDF presentation of theory documents. +HTML presentation of PIDE document content. */ package isabelle @@ -14,6 +14,8 @@ { /** HTML documents **/ + /* HTML context */ + val fonts_path = Path.explode("fonts") sealed case class HTML_Document(title: String, content: String) @@ -74,7 +76,7 @@ language = Markup.Elements(Markup.Language.DOCUMENT)) - /* HTML */ + /* HTML output */ private val div_elements = Set(HTML.div.name, HTML.pre.name, HTML.par.name, HTML.list.name, HTML.enum.name, @@ -169,120 +171,7 @@ - /** PDF LaTeX documents **/ - - /* document info */ - - abstract class Document_Name - { - def name: String - def path: Path = Path.basic(name) - - override def toString: String = name - } - - object Document_Variant - { - def parse(name: String, tags: String): Document_Variant = - Document_Variant(name, Library.space_explode(',', tags)) - - def parse(opt: String): Document_Variant = - Library.space_explode('=', opt) match { - case List(name) => Document_Variant(name, Nil) - case List(name, tags) => parse(name, tags) - case _ => error("Malformed document variant: " + quote(opt)) - } - } - - sealed case class Document_Variant(name: String, tags: List[String]) extends Document_Name - { - def print_tags: String = tags.mkString(",") - def print: String = if (tags.isEmpty) name else name + "=" + print_tags - - 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 + "}" - })) - } - - sealed case class Document_Input(name: String, sources: SHA1.Digest) - extends Document_Name - - sealed case class Document_Output(name: String, sources: SHA1.Digest, log_xz: Bytes, pdf: Bytes) - extends Document_Name - { - def log: String = log_xz.uncompress().text - def log_lines: List[String] = split_lines(log) - - def write(db: SQL.Database, session_name: String): Unit = - write_document(db, session_name, this) - } - - - /* SQL data model */ - - object Data - { - val session_name = SQL.Column.string("session_name").make_primary_key - val name = SQL.Column.string("name").make_primary_key - val sources = SQL.Column.string("sources") - val log_xz = SQL.Column.bytes("log_xz") - val pdf = SQL.Column.bytes("pdf") - - val table = SQL.Table("isabelle_documents", List(session_name, name, sources, log_xz, pdf)) - - def where_equal(session_name: String, name: String = ""): SQL.Source = - "WHERE " + Data.session_name.equal(session_name) + - (if (name == "") "" else " AND " + Data.name.equal(name)) - } - - def read_documents(db: SQL.Database, session_name: String): List[Document_Input] = - { - val select = Data.table.select(List(Data.name, Data.sources), Data.where_equal(session_name)) - db.using_statement(select)(stmt => - stmt.execute_query().iterator(res => - { - val name = res.string(Data.name) - val sources = res.string(Data.sources) - Document_Input(name, SHA1.fake(sources)) - }).toList) - } - - def read_document(db: SQL.Database, session_name: String, name: String): Option[Document_Output] = - { - val select = Data.table.select(sql = Data.where_equal(session_name, name)) - db.using_statement(select)(stmt => - { - val res = stmt.execute_query() - if (res.next()) { - val name = res.string(Data.name) - val sources = res.string(Data.sources) - val log_xz = res.bytes(Data.log_xz) - val pdf = res.bytes(Data.pdf) - Some(Document_Output(name, SHA1.fake(sources), log_xz, pdf)) - } - else None - }) - } - - def write_document(db: SQL.Database, session_name: String, doc: Document_Output): Unit = - { - db.using_statement(Data.table.insert())(stmt => - { - stmt.string(1) = session_name - stmt.string(2) = doc.name - stmt.string(3) = doc.sources.toString - stmt.bytes(4) = doc.log_xz - stmt.bytes(5) = doc.pdf - stmt.execute() - }) - } - + /** HTML presentation **/ /* presentation context */ @@ -311,9 +200,6 @@ } - - /** HTML presentation **/ - /* maintain chapter index */ private val sessions_path = Path.basic(".sessions") @@ -498,7 +384,7 @@ val documents = for { doc <- info.document_variants - document <- db_context.input_database(session)(read_document(_, _, doc.name)) + document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name)) } yield { if (verbose) progress.echo("Presenting document " + session + "/" + doc.name) Bytes.write(session_dir + doc.path.pdf, document.pdf) @@ -613,259 +499,4 @@ html_context.head(title, List(HTML.par(view_links))) :: html_context.contents("Theories", theories)) } - - - - /** build documents **/ - - val session_tex_path = Path.explode("session.tex") - - 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) - - class Build_Error(val log_lines: List[String], val message: String) - extends Exn.User_Error(message) - - def build_documents( - session: String, - deps: Sessions.Deps, - db_context: Sessions.Database_Context, - progress: Progress = new Progress, - output_sources: Option[Path] = None, - output_pdf: Option[Path] = None, - verbose: Boolean = false, - verbose_latex: Boolean = false): List[Document_Output] = - { - /* session info */ - - val info = deps.sessions_structure(session) - val hierarchy = deps.sessions_structure.hierarchy(session) - val options = info.options - val base = deps(session) - val graph_pdf = graphview.Graph_File.make_pdf(options, base.session_graph_display) - - - /* prepare document directory */ - - lazy val tex_files = - for (name <- base.session_theories ::: base.document_theories) - yield { - val entry = db_context.get_export(hierarchy, name.theory, document_tex_name(name)) - Path.basic(tex_name(name)) -> entry.uncompressed - } - - def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) = - { - 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"), doc.latex_sty) - for ((base_dir, src) <- info.document_files) { - Isabelle_System.copy_file_base(info.dir + base_dir, src, doc_dir) - } - - File.write(doc_dir + session_tex_path, - Library.terminate_lines( - base.session_theories.map(name => "\\input{" + tex_name(name) + "}"))) - - for ((path, tex) <- tex_files) Bytes.write(doc_dir + path, tex) - - val root1 = "root_" + doc.name - val root = if ((doc_dir + Path.explode(root1).tex).is_file) root1 else "root" - - (doc_dir, root) - } - - def prepare_dir2(dir: Path, doc: Document_Variant): Unit = - { - val doc_dir = dir + Path.basic(doc.name) - - // non-deterministic, but irrelevant - Bytes.write(doc_dir + session_graph_path, graph_pdf) - } - - - /* produce documents */ - - val documents = - for (doc <- info.documents) - yield { - Isabelle_System.with_tmp_dir("document")(tmp_dir => - { - progress.echo("Preparing " + session + "/" + doc.name + " ...") - val start = Time.now() - - - // prepare sources - - val (doc_dir, root) = prepare_dir1(tmp_dir, doc) - val digests = File.find_files(doc_dir.file, follow_links = true).map(SHA1.digest) - val sources = SHA1.digest_set(digests) - prepare_dir2(tmp_dir, doc) - - for (dir <- output_sources) { - prepare_dir1(dir, doc) - prepare_dir2(dir, doc) - } - - - // old document from database - - val old_document = - for { - old_doc <- db_context.input_database(session)(read_document(_, _, doc.name)) - if old_doc.sources == sources - } - yield { - Bytes.write(doc_dir + doc.path.pdf, old_doc.pdf) - old_doc - } - - old_document getOrElse { - // bash scripts - - def root_bash(ext: String): String = Bash.string(root + "." + ext) - - def latex_bash(fmt: String = "pdf", ext: String = "tex"): String = - "isabelle latex -o " + Bash.string(fmt) + " " + Bash.string(root + "." + ext) - - def bash(items: String*): Process_Result = - progress.bash(items.mkString(" && "), cwd = doc_dir.file, - echo = verbose_latex, watchdog = Time.seconds(0.5)) - - - // prepare document - - val result = - if ((doc_dir + Path.explode("build")).is_file) { - bash("./build pdf " + Bash.string(doc.name)) - } - else { - bash( - latex_bash(), - "{ [ ! -f " + root_bash("bib") + " ] || " + latex_bash("bbl") + "; }", - "{ [ ! -f " + root_bash("idx") + " ] || " + latex_bash("idx") + "; }", - latex_bash(), - latex_bash()) - } - - - // result - - val root_pdf = Path.basic(root).pdf - val result_path = doc_dir + root_pdf - - val log_lines = result.out_lines ::: result.err_lines - - val errors = - (if (result.ok) Nil else List(result.err)) ::: - Latex.latex_errors(doc_dir, root) ::: - Bibtex.bibtex_errors(doc_dir, root) - - if (errors.nonEmpty) { - val message = - Exn.cat_message( - (errors ::: List("Failed to build document " + quote(doc.name))):_*) - throw new Build_Error(log_lines, message) - } - else if (!result_path.is_file) { - val message = "Bad document result: expected to find " + root_pdf - throw new Build_Error(log_lines, message) - } - else { - val stop = Time.now() - val timing = stop - start - progress.echo("Finished " + session + "/" + doc.name + - " (" + timing.message_hms + " elapsed time)") - - val log_xz = Bytes(cat_lines(log_lines)).compress() - val pdf = Bytes.read(result_path) - Document_Output(doc.name, sources, log_xz, pdf) - } - } - }) - } - - for (dir <- output_pdf; doc <- documents) { - Isabelle_System.make_directory(dir) - val path = dir + doc.path.pdf - Bytes.write(path, doc.pdf) - progress.echo("Document at " + path.absolute) - } - - documents - } - - - /* Isabelle tool wrapper */ - - val isabelle_tool = - Isabelle_Tool("document", "prepare session theory document", Scala_Project.here, args => - { - var output_sources: Option[Path] = None - var output_pdf: Option[Path] = None - var verbose_latex = false - var dirs: List[Path] = Nil - var options = Options.init() - var verbose_build = false - - val getopts = Getopts( - """ -Usage: isabelle document [OPTIONS] SESSION - - Options are: - -O DIR output directory for LaTeX sources and resulting PDF - -P DIR output directory for resulting PDF - -S DIR output directory for LaTeX sources - -V verbose latex - -d DIR include session directory - -o OPTION override Isabelle system OPTION (via NAME=VAL or NAME) - -v verbose build - - Prepare the theory document of a session. -""", - "O:" -> (arg => - { - val dir = Path.explode(arg) - output_sources = Some(dir) - output_pdf = Some(dir) - }), - "P:" -> (arg => { output_pdf = Some(Path.explode(arg)) }), - "S:" -> (arg => { output_sources = Some(Path.explode(arg)) }), - "V" -> (_ => verbose_latex = true), - "d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))), - "o:" -> (arg => options = options + arg), - "v" -> (_ => verbose_build = true)) - - val more_args = getopts(args) - val session = - more_args match { - case List(a) => a - case _ => getopts.usage() - } - - val progress = new Console_Progress(verbose = verbose_build) - val store = Sessions.store(options) - - progress.interrupt_handler { - val res = - Build.build(options, selection = Sessions.Selection.session(session), - dirs = dirs, progress = progress, verbose = verbose_build) - if (!res.ok) error("Failed to build session " + quote(session)) - - val deps = - Sessions.load_structure(options + "document=pdf", dirs = dirs). - selection_deps(Sessions.Selection.session(session)) - - if (output_sources.isEmpty && output_pdf.isEmpty) { - progress.echo_warning("No output directory") - } - - using(store.open_database_context())(db_context => - build_documents(session, deps, db_context, progress = progress, - output_sources = output_sources, output_pdf = output_pdf, - verbose = true, verbose_latex = verbose_latex)) - } - }) } diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/Thy/sessions.scala Mon May 17 16:15:25 2021 +0200 @@ -514,11 +514,11 @@ case doc => error("Bad document specification " + quote(doc)) } - def document_variants: List[Presentation.Document_Variant] = + def document_variants: List[Document_Build.Document_Variant] = { val variants = Library.space_explode(':', options.string("document_variants")). - map(Presentation.Document_Variant.parse) + map(Document_Build.Document_Variant.parse) val dups = Library.duplicates(variants.map(_.name)) if (dups.nonEmpty) error("Duplicate document variants: " + commas_quote(dups)) @@ -526,7 +526,7 @@ variants } - def documents: List[Presentation.Document_Variant] = + def documents: List[Document_Build.Document_Variant] = { val variants = document_variants if (!document_enabled || document_files.isEmpty) Nil else variants @@ -1429,10 +1429,10 @@ db.using_statement( Export.Data.table.delete(Export.Data.session_name.where_equal(name)))(_.execute()) - db.create_table(Presentation.Data.table) + db.create_table(Document_Build.Data.table) db.using_statement( - Presentation.Data.table.delete( - Presentation.Data.session_name.where_equal(name)))(_.execute()) + Document_Build.Data.table.delete( + Document_Build.Data.session_name.where_equal(name)))(_.execute()) } } diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Mon May 17 16:15:25 2021 +0200 @@ -447,7 +447,7 @@ using(store.open_database_context())(db_context => { val documents = - Presentation.build_documents(session_name, deps, db_context, + Document_Build.build_documents(session_name, deps, db_context, output_sources = info.document_output, output_pdf = info.document_output, progress = progress, @@ -460,7 +460,7 @@ else (Nil, Nil) } catch { - case exn: Presentation.Build_Error => (exn.log_lines, List(exn.message)) + case exn: Document_Build.Build_Error => (exn.log_lines, List(exn.message)) case Exn.Interrupt.ERROR(msg) => (Nil, List(msg)) } diff -r 2f4cb9cb087f -r ecb31c3bf980 src/Pure/build-jars --- a/src/Pure/build-jars Mon May 17 15:01:37 2021 +0200 +++ b/src/Pure/build-jars Mon May 17 16:15:25 2021 +0200 @@ -154,6 +154,7 @@ src/Pure/System/system_channel.scala src/Pure/System/tty_loop.scala src/Pure/Thy/bibtex.scala + src/Pure/Thy/document_build.scala src/Pure/Thy/export.scala src/Pure/Thy/export_theory.scala src/Pure/Thy/file_format.scala