--- 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+) \.\.\.$""")
--- 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)