--- a/NEWS Mon Nov 08 12:45:35 2021 +0100
+++ b/NEWS Mon Nov 08 13:51:24 2021 +0100
@@ -116,6 +116,9 @@
explicitly requires document_build=build. Minor INCOMPATIBILITY, need to
adjust session ROOT options.
+* Option "document_echo" informs about document file names during
+session presentation.
+
* The command-line tool "isabelle latex" has been discontinued,
INCOMPATIBILITY for old document build scripts.
--- a/etc/options Mon Nov 08 12:45:35 2021 +0100
+++ b/etc/options Mon Nov 08 13:51:24 2021 +0100
@@ -9,6 +9,8 @@
-- "build PDF document (enabled for \"pdf\" or \"true\", disabled for \"\" or \"false\")"
option document_output : string = ""
-- "document output directory"
+option document_echo : bool = false
+ -- "inform about document file names during session presentation"
option document_variants : string = "document"
-- "alternative document variants (separated by colons)"
option document_tags : string = ""
--- a/src/Pure/Thy/presentation.scala Mon Nov 08 12:45:35 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Mon Nov 08 13:51:24 2021 +0100
@@ -406,8 +406,10 @@
doc <- info.document_variants
document <- db_context.input_database(session)(Document_Build.read_document(_, _, doc.name))
} yield {
+ val doc_path = (session_dir + doc.path.pdf).expand
if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
- Bytes.write(session_dir + doc.path.pdf, document.pdf)
+ if (options.bool("document_echo")) progress.echo("Document at " + doc_path)
+ Bytes.write(doc_path, document.pdf)
doc
}