# HG changeset patch
# User wenzelm
# Date 1636375884 -3600
# Node ID 015282fb3e31cabdb42866a3746e0088ffd8e867
# Parent  161e84e6b40acf630bcdc9a7f2cac8509c5e9c49
clarified messages, depending on option "document_echo";

diff -r 161e84e6b40a -r 015282fb3e31 NEWS
--- 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.
 
diff -r 161e84e6b40a -r 015282fb3e31 etc/options
--- 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 = ""
diff -r 161e84e6b40a -r 015282fb3e31 src/Pure/Thy/presentation.scala
--- 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
       }