# HG changeset patch
# User wenzelm
# Date 1606144702 -3600
# Node ID 45cd55248ffdea5a8eaeac89a291c438ab76576c
# Parent  0116e487e4fe8a252baa39b935691d825d99ac39
clarified messages;

diff -r 0116e487e4fe -r 45cd55248ffd src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Nov 23 16:02:04 2020 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Nov 23 16:18:22 2020 +0100
@@ -485,7 +485,7 @@
     val Session_Finished1 =
       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
     val Session_Finished2 =
-      new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
+      new Regex("""^Finished ([^\s/]+) \((\d+):(\d+):(\d+) elapsed time.*$""")
     val Session_Timing =
       new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
diff -r 0116e487e4fe -r 45cd55248ffd src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Mon Nov 23 16:02:04 2020 +0100
+++ b/src/Pure/Thy/presentation.scala	Mon Nov 23 16:18:22 2020 +0100
@@ -499,7 +499,7 @@
       yield {
         Isabelle_System.with_tmp_dir("document")(tmp_dir =>
         {
-          progress.echo_document("Building document " + session + "/" + doc.name + " ...")
+          progress.echo_document("Preparing " + session + "/" + doc.name + " ...")
           val start = Time.now()
 
 
@@ -574,7 +574,7 @@
             else {
               val stop = Time.now()
               val timing = stop - start
-              progress.echo_document("Finished document " + session + "/" + doc.name +
+              progress.echo_document("Finished " + session + "/" + doc.name +
                 " (" + timing.message_hms + " elapsed time)")
 
               doc.set_sources(sources) -> Bytes.read(result_path)