# HG changeset patch # User wenzelm # Date 1709924601 -3600 # Node ID 11fa48986f37530cc2a3ddd40d40ee81844dfe08 # Parent 56f506c556f160405b3b0ab44f2f68471ce10801 more accurate patterns --- reverting unused fc3ba0a1c82f; diff -r 56f506c556f1 -r 11fa48986f37 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Fri Mar 08 19:18:39 2024 +0100 +++ b/src/Pure/Admin/build_log.scala Fri Mar 08 20:03:21 2024 +0100 @@ -452,9 +452,9 @@ 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_Started1 = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""") - val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on ([^\s/]+)/?(\d+)\+?(\S+)\)? \.\.\.$""") + val Session_Started2 = new Regex("""^(?:Running|Building) (\S+) \(?on ([^\s/]+)[^)]*\)? \.\.\.$""") val Session_Started3 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+)\) \.\.\.$""") - val Session_Started4 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+) on ([^\s/]+)/?(\d+)\+?(\S+)\) \.\.\.$""") + val Session_Started4 = new Regex("""^(?:Running|Building) (\S+) \(started (\d+):(\d+):(\d+) on ([^\s/]+)[^)]*\) \.\.\.$""") val Sources = new Regex("""^Sources (\S+) (\S{""" + SHA1.digest_length + """})$""") val Heap = new Regex("""^Heap (\S+) \((\d+) bytes\)$""") @@ -501,14 +501,14 @@ case Session_Started1(name) => started += (name -> None) - case Session_Started2(name, hostname, _, _) => + case Session_Started2(name, hostname) => started += (name -> None) hostnames += (name -> hostname) case Session_Started3(name, Value.Int(t1), Value.Int(t2), Value.Int(t3)) => started += (name -> Some(Time.hms(t1, t2, t3))) - case Session_Started4(name, Value.Int(t1), Value.Int(t2), Value.Int(t3), hostname, _, _) => + case Session_Started4(name, Value.Int(t1), Value.Int(t2), Value.Int(t3), hostname) => started += (name -> Some(Time.hms(t1, t2, t3))) hostnames += (name -> hostname)