--- a/src/Pure/Thy/presentation.scala Wed Nov 18 15:52:12 2020 +0100
+++ b/src/Pure/Thy/presentation.scala Wed Nov 18 21:34:13 2020 +0100
@@ -16,18 +16,24 @@
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))
+ 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] = Nil)
+ sealed case class Document_Variant(name: String, tags: List[String], sources: String = "")
{
- def print: String = if (tags.isEmpty) name else name + "=" + tags.mkString(",")
+ def print_tags: String = tags.mkString(",")
+ def print: String = if (tags.isEmpty) name else name + "=" + print_tags
+
def path: Path = Path.basic(name)
+
def latex_sty: String =
Library.terminate_lines(
tags.map(tag =>
@@ -37,6 +43,71 @@
case '+' :: cs => "\\isakeeptag{" + cs.mkString + "}"
case cs => "\\isakeeptag{" + cs.mkString + "}"
}))
+
+ def set_sources(s: String): Document_Variant = copy(sources = s)
+ }
+
+
+ /* 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 tags = SQL.Column.string("tags")
+ val sources = SQL.Column.string("sources")
+ val pdf = SQL.Column.bytes("pdf")
+
+ val table = SQL.Table("isabelle_documents", List(session_name, name, tags, sources, 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_document_variants(db: SQL.Database, session_name: String): List[Document_Variant] =
+ {
+ val select =
+ Data.table.select(List(Data.name, Data.tags, Data.sources), Data.where_equal(session_name))
+ db.using_statement(select)(stmt =>
+ stmt.execute_query().iterator(res =>
+ {
+ val name = res.string(Data.name)
+ val tags = res.string(Data.tags)
+ val sources = res.string(Data.sources)
+ Document_Variant.parse(name, tags).set_sources(sources)
+ }).toList)
+ }
+
+ def read_document(db: SQL.Database, session_name: String, name: String)
+ : Option[(Document_Variant, Bytes)] =
+ {
+ 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 tags = res.string(Data.tags)
+ val sources = res.string(Data.sources)
+ val pdf = res.bytes(Data.pdf)
+ Some(Document_Variant.parse(name, tags).set_sources(sources) -> pdf)
+ }
+ else None
+ })
+ }
+
+ def write_document(db: SQL.Database, session_name: String, doc: Document_Variant, pdf: Bytes)
+ {
+ db.using_statement(Data.table.insert())(stmt =>
+ {
+ stmt.string(1) = session_name
+ stmt.string(2) = doc.name
+ stmt.string(3) = doc.print_tags
+ stmt.string(4) = doc.sources
+ stmt.bytes(5) = pdf
+ stmt.execute()
+ })
}
@@ -304,7 +375,6 @@
deps: Sessions.Deps,
store: Sessions.Store,
progress: Progress = new Progress,
- presentation: Context = Context.none,
verbose: Boolean = false,
verbose_latex: Boolean = false): List[(Document_Variant, Bytes)] =
{
@@ -327,7 +397,7 @@
}
)
- def prepare_dir(dir: Path, doc: Document_Variant): (Path, String) =
+ def prepare_dir1(dir: Path, doc: Document_Variant): (Path, String) =
{
val doc_dir = dir + Path.basic(doc.name)
Isabelle_System.make_directory(doc_dir)
@@ -335,7 +405,6 @@
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) File.copy_base(info.dir + base_dir, src, doc_dir)
- Bytes.write(doc_dir + session_graph_path, graph_pdf)
File.write(doc_dir + session_tex_path,
Library.terminate_lines(
@@ -349,6 +418,14 @@
(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 */
@@ -359,72 +436,84 @@
yield {
Isabelle_System.with_tmp_dir("document")(tmp_dir =>
{
- val (doc_dir, root) = prepare_dir(tmp_dir, doc)
- doc_output.foreach(prepare_dir(_, doc))
-
-
- // bash scripts
+ // prepare sources
- def root_bash(ext: String): String = Bash.string(root + "." + ext)
+ 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(cat_lines(digests.map(_.toString).sorted)).toString
+ prepare_dir2(tmp_dir, doc)
- 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))
+ doc_output.foreach(prepare_dir1(_, doc))
+ doc_output.foreach(prepare_dir2(_, doc))
- // prepare document
+ // old document from database
- 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())
- }
+ val old_document =
+ using(store.open_database(session))(db =>
+ for {
+ document@(doc, pdf) <- read_document(db, session, doc.name)
+ if doc.sources == sources
+ }
+ yield {
+ Bytes.write(doc_dir + doc.path.pdf, pdf)
+ document
+ })
+
+ 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))
- // result
+ // prepare document
- val root_pdf = Path.basic(root).pdf
- val result_path = doc_dir + root_pdf
+ 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())
+ }
+
- if (!result.ok) {
- 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))
+ // result
+
+ val root_pdf = Path.basic(root).pdf
+ val result_path = doc_dir + root_pdf
+
+ if (!result.ok) {
+ 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))
+ }
+ else if (!result_path.is_file) {
+ error("Bad document result: expected to find " + root_pdf)
+ }
+ else doc.set_sources(sources) -> Bytes.read(result_path)
}
- else if (!result_path.is_file) {
- error("Bad document result: expected to find " + root_pdf)
- }
- else doc -> Bytes.read(result_path)
})
}
- def output(dir: Path)
- {
- Isabelle_System.make_directory(dir)
- for ((doc, pdf) <- documents) {
- val path = dir + doc.path.pdf
- Bytes.write(path, pdf)
- progress.echo_document(path)
- }
+ for (dir <- doc_output; (doc, pdf) <- documents) {
+ val path = dir + doc.path.pdf
+ Bytes.write(path, pdf)
+ progress.echo_document(path)
}
- if (presentation.enabled(info) || doc_output.isEmpty) {
- output(presentation.dir(store, info))
- }
-
- doc_output.foreach(output)
-
documents
}
@@ -434,7 +523,6 @@
val isabelle_tool =
Isabelle_Tool("document", "prepare session theory document", args =>
{
- var presentation = Presentation.Context.none
var verbose_latex = false
var dirs: List[Path] = Nil
var options = Options.init()
@@ -445,7 +533,6 @@
Usage: isabelle document [OPTIONS] SESSION
Options are:
- -P DIR enable HTML/PDF presentation in directory (":" for default)
-O set option "document_output", relative to current directory
-V verbose latex
-d DIR include session directory
@@ -454,7 +541,6 @@
Prepare the theory document of a session.
""",
- "P:" -> (arg => presentation = Context.make(arg)),
"O:" -> (arg => options += ("document_output=" + Path.explode(arg).absolute.implode)),
"V" -> (_ => verbose_latex = true),
"d:" -> (arg => dirs = dirs ::: List(Path.explode(arg))),
@@ -481,8 +567,12 @@
Sessions.load_structure(options + "document=pdf", dirs = dirs).
selection_deps(Sessions.Selection.session(session))
+ if (deps.sessions_structure(session).document_output.isEmpty) {
+ progress.echo_warning("No document_output")
+ }
+
build_documents(session, deps, store, progress = progress,
- presentation = presentation, verbose = true, verbose_latex = verbose_latex)
+ verbose = true, verbose_latex = verbose_latex)
}
})
}
--- a/src/Pure/Tools/build.scala Wed Nov 18 15:52:12 2020 +0100
+++ b/src/Pure/Tools/build.scala Wed Nov 18 21:34:13 2020 +0100
@@ -360,19 +360,30 @@
val document_errors =
try {
if (build_errors.isInstanceOf[Exn.Res[_]] && process_result.ok) {
- if (info.documents.nonEmpty) {
- val document_progress =
- new Progress {
- override def echo(msg: String): Unit =
- document_output.synchronized { document_output += msg }
- override def echo_document(path: Path): Unit =
- progress.echo_document(path)
- }
- Presentation.build_documents(session_name, deps, store, verbose = verbose,
- verbose_latex = true, progress = document_progress)
- }
+ val documents =
+ if (info.documents.isEmpty) Nil
+ else {
+ val document_progress =
+ new Progress {
+ override def echo(msg: String): Unit =
+ document_output.synchronized { document_output += msg }
+ override def echo_document(path: Path): Unit =
+ progress.echo_document(path)
+ }
+ val documents =
+ Presentation.build_documents(session_name, deps, store, verbose = verbose,
+ verbose_latex = true, progress = document_progress)
+ using(store.open_database(session_name, output = true))(db =>
+ for ((doc, pdf) <- documents) {
+ db.transaction {
+ Presentation.write_document(db, session_name, doc, pdf)
+ }
+ })
+ documents
+ }
if (presentation.enabled(info)) {
val dir = Presentation.session_html(session_name, deps, store, presentation)
+ for ((doc, pdf) <- documents) Bytes.write(dir + doc.path.pdf, pdf)
if (verbose) progress.echo("Browser info at " + dir.absolute)
}
}