# HG changeset patch
# User wenzelm
# Date 1609542325 -3600
# Node ID 38528017e4c82074035ffe70ba8d34d07a2159e2
# Parent  f602a380e4f21c09411d9ab18b46d482a8deff04
more verbosity for potentially bulky presentation;

diff -r f602a380e4f2 -r 38528017e4c8 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Jan 01 23:35:09 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Sat Jan 02 00:05:25 2021 +0100
@@ -375,6 +375,7 @@
     deps: Sessions.Deps,
     db_context: Sessions.Database_Context,
     progress: Progress = new Progress,
+    verbose: Boolean = false,
     html_context: HTML_Context,
     presentation: Context)
   {
@@ -393,7 +394,11 @@
       for {
         doc <- info.document_variants
         document <- db_context.input_database(session)(read_document(_, _, doc.name))
-      } yield { Bytes.write(session_dir + doc.path.pdf, document.pdf); doc }
+      } yield {
+        if (verbose) progress.echo("Presenting document " + session + "/" + doc.name)
+        Bytes.write(session_dir + doc.path.pdf, document.pdf)
+        doc
+      }
 
     val links =
     {
@@ -433,6 +438,7 @@
       for (thy_name <- base.session_theories)
       yield {
         progress.expose_interrupt()
+        if (verbose) progress.echo("Presenting theory " + thy_name)
 
         val syntax = base.theory_syntax(thy_name)
         val keywords = syntax.keywords
@@ -481,6 +487,8 @@
                   " in theory " + thy_name1 + " vs. " + thy_name)
             }
 
+            if (verbose) progress.echo("Presenting file " + src_path)
+
             val file_path = session_dir + Path.explode(file_name)
             html_context.init_fonts(file_path.dir)
 
diff -r f602a380e4f2 -r 38528017e4c8 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jan 01 23:35:09 2021 +0100
+++ b/src/Pure/Tools/build.scala	Sat Jan 02 00:05:25 2021 +0100
@@ -514,7 +514,8 @@
             progress.expose_interrupt()
             progress.echo("Presenting " + session_name + " ...")
             Presentation.session_html(
-              resources, session_name, deps, db_context, progress, html_context, presentation)
+              resources, session_name, deps, db_context, progress = progress,
+              verbose = verbose, html_context = html_context, presentation = presentation)
           })
 
         val browser_chapters =