clarified messages;
authorwenzelm
Thu, 19 Nov 2020 22:05:34 +0100
changeset 72665 7e5102e11c5e
parent 72664 0d3224b3a92c
child 72666 945cee776e79
clarified messages;
src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Thu Nov 19 21:59:17 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Thu Nov 19 22:05:34 2020 +0100
@@ -436,6 +436,10 @@
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
+          progress.echo_document("Building document " + session + "/" + doc.name + " ...")
+          val start = Time.now()
+
+
           // prepare sources
 
           val (doc_dir, root) = prepare_dir1(tmp_dir, doc)
@@ -503,7 +507,14 @@
             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 {
+              val stop = Time.now()
+              val timing = stop - start
+              progress.echo_document("Finished document " + session + "/" + doc.name +
+                " (" + timing.message_hms + " elapsed time)")
+
+              doc.set_sources(sources) -> Bytes.read(result_path)
+            }
           }
         })
       }