# HG changeset patch # User wenzelm # Date 1508350497 -7200 # Node ID e7635ea96988250af420190ddf321c4705901a24 # Parent 486f4af28db9a218be221a196fbe2feacdd225e7 tuned output; diff -r 486f4af28db9 -r e7635ea96988 src/Pure/Admin/build_status.scala --- a/src/Pure/Admin/build_status.scala Wed Oct 18 19:53:19 2017 +0200 +++ b/src/Pure/Admin/build_status.scala Wed Oct 18 20:14:57 2017 +0200 @@ -96,6 +96,7 @@ entry.stored_heap > 0) } sealed case class Entry( + chapter: String, pull_date: Date, isabelle_version: String, afp_version: String, @@ -112,10 +113,11 @@ def present_errors(name: String): XML.Body = { - if (errors.isEmpty) HTML.text(name + print_versions(isabelle_version, afp_version)) + if (errors.isEmpty) + HTML.text(name + print_version(isabelle_version, afp_version, chapter)) else { HTML.tooltip_errors(HTML.text(name), errors.map(s => HTML.text(Symbol.decode(s)))) :: - HTML.text(print_versions(isabelle_version, afp_version)) + HTML.text(print_version(isabelle_version, afp_version, chapter)) } } } @@ -125,11 +127,12 @@ def path: Path = Path.basic(name) } - def print_versions(isabelle_version: String, afp_version: String): String = + def print_version( + isabelle_version: String, afp_version: String = "", chapter: String = "AFP"): String = { val body = proper_string(isabelle_version).map("Isabelle/" + _).toList ::: - proper_string(afp_version).map("AFP/" + _).toList + (if (chapter == "AFP") proper_string(afp_version).map("AFP/" + _) else None).toList if (body.isEmpty) "" else body.mkString(" (", ", ", ")") } @@ -164,6 +167,7 @@ Build_Log.Settings.ISABELLE_BUILD_OPTIONS, Build_Log.Settings.ML_PLATFORM, Build_Log.Data.session_name, + Build_Log.Data.chapter, Build_Log.Data.threads, Build_Log.Data.timing_elapsed, Build_Log.Data.timing_cpu, @@ -186,6 +190,7 @@ val res = stmt.execute_query() while (res.next()) { val session_name = res.string(Build_Log.Data.session_name) + val chapter = res.string(Build_Log.Data.chapter) val threads = { val threads1 = @@ -214,10 +219,12 @@ ML_Statistics( if (ml_statistics) Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics)) - else Nil, heading = session_name + print_versions(isabelle_version, afp_version)) + else Nil, + heading = session_name + print_version(isabelle_version, afp_version, chapter)) val entry = Entry( + chapter = chapter, pull_date = res.date(Build_Log.Data.pull_date(afp)), isabelle_version = isabelle_version, afp_version = afp_version,