# HG changeset patch # User wenzelm # Date 1585503779 -7200 # Node ID 5a4ccef7f310998eb908ddc4510e7c99e51969d6 # Parent e33f6e5f86b679c28eef47a3cf0a9fb5424c9e90 more explicit type Protocol_Message.Marker; tuned; diff -r e33f6e5f86b6 -r 5a4ccef7f310 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun Mar 29 13:25:59 2020 +0200 +++ b/src/Pure/Admin/build_history.scala Sun Mar 29 19:42:59 2020 +0200 @@ -18,7 +18,6 @@ val engine = "build_history" val log_prefix = engine + "_" - val META_INFO_MARKER = "\fmeta_info = " /* augment settings */ @@ -282,8 +281,7 @@ val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => - Build_Log.Log_File.print_props(Build_Log.THEORY_TIMING_MARKER, - (Build_Log.SESSION_NAME, session_name) :: ps)) + Build_Log.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } @@ -357,10 +355,10 @@ build_out_progress.echo("Writing log file " + log_path.ext("xz") + " ...") File.write_xz(log_path.ext("xz"), terminate_lines( - Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: build_result.out_lines ::: + Build_Log.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: - ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: - session_errors.map(Build_Log.Log_File.print_props(Build_Log.ERROR_MESSAGE_MARKER, _)) ::: + ml_statistics.map(Build_Log.ML_Statistics_Marker.apply) ::: + session_errors.map(Build_Log.Error_Message_Marker.apply) ::: heap_sizes), XZ.options(6)) diff -r e33f6e5f86b6 -r 5a4ccef7f310 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sun Mar 29 13:25:59 2020 +0200 +++ b/src/Pure/Admin/build_log.scala Sun Mar 29 19:42:59 2020 +0200 @@ -187,12 +187,6 @@ Date.Format.make(fmts, tune) } - - - /* inlined content */ - - def print_props(marker: String, props: Properties.T): String = - marker + YXML.string_of_body(XML.Encode.properties(Properties.encode_lines(props))) } class Log_File private(val name: String, val lines: List[String]) @@ -217,13 +211,13 @@ } - /* inlined content */ + /* inlined text */ - def find[A](f: String => Option[A]): Option[A] = - lines.iterator.map(f).find(_.isDefined).map(_.get) + def filter(Marker: Protocol_Message.Marker): List[String] = + for (Marker(text) <- lines) yield text - def find_line(marker: String): Option[String] = - find(Library.try_unprefix(marker, _)) + def find(Marker: Protocol_Message.Marker): Option[String] = + lines.collectFirst({ case Marker(text) => text }) def find_match(regexes: List[Regex]): Option[String] = regexes match { @@ -249,25 +243,17 @@ /* properties (YXML) */ - val xml_cache = XML.make_cache() + val xml_cache: XML.Cache = XML.make_cache() def parse_props(text: String): Properties.T = - try { - xml_cache.props(Properties.decode_lines(XML.Decode.properties(YXML.parse_body(text)))) - } + try { xml_cache.props(XML.Decode.properties(YXML.parse_body(text))) } catch { case _: XML.Error => log_file.err("malformed properties") } - def filter_lines(marker: String): List[String] = - for (line <- lines; s <- Library.try_unprefix(marker, line)) yield s - - def filter_props(marker: String): List[Properties.T] = - for (s <- filter_lines(marker) if YXML.detect(s)) yield parse_props(s) + def filter_props(marker: Protocol_Message.Marker): List[Properties.T] = + for (text <- filter(marker) if YXML.detect(text)) yield parse_props(text) - def find_props(marker: String): Option[Properties.T] = - find_line(marker) match { - case Some(text) if YXML.detect(text) => Some(parse_props(text)) - case _ => None - } + def find_props(marker: Protocol_Message.Marker): Option[Properties.T] = + for (text <- find(marker) if YXML.detect(text)) yield parse_props(text) /* parse various formats */ @@ -401,9 +387,8 @@ } log_file.lines match { - case line :: _ if line.startsWith(Build_History.META_INFO_MARKER) => - Meta_Info(log_file.find_props(Build_History.META_INFO_MARKER).get, - log_file.get_all_settings) + case line :: _ if Meta_Info_Marker.test_yxml(line) => + Meta_Info(log_file.find_props(Meta_Info_Marker).get, log_file.get_all_settings) case Identify.Start(log_file.Strict_Date(start)) :: _ => parse(Identify.engine(log_file), "", start, Identify.No_End, @@ -446,9 +431,13 @@ /** build info: toplevel output of isabelle build or Admin/build_history **/ - val THEORY_TIMING_MARKER = "\ftheory_timing = " - val ML_STATISTICS_MARKER = "\fML_statistics = " - val ERROR_MESSAGE_MARKER = "\ferror_message = " + val Meta_Info_Marker = Protocol_Message.Marker("meta_info") + val Timing_Marker = Protocol_Message.Marker("Timing") + val Command_Timing_Marker = Protocol_Message.Marker("command_timing") + val Theory_Timing_Marker = Protocol_Message.Marker("theory_timing") + val ML_Statistics_Marker = Protocol_Message.Marker("ML_statistics") + val Task_Statistics_Marker = Protocol_Message.Marker("task_statistics") + val Error_Message_Marker = Protocol_Message.Marker("error_message") val SESSION_NAME = "session_name" object Session_Status extends Enumeration @@ -514,9 +503,7 @@ object Theory_Timing { def unapply(line: String): Option[(String, (String, Timing))] = - { - val line1 = line.replace('~', '-') - Library.try_unprefix(THEORY_TIMING_MARKER, line1).map(log_file.parse_props(_)) match { + Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match { case Some((SESSION_NAME, name) :: props) => (props, props) match { case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t)) @@ -524,7 +511,6 @@ } case _ => None } - } } var chapter = Map.empty[String, String] @@ -586,24 +572,24 @@ case Heap(name, Value.Long(size)) => heap_sizes += (name -> size) - case _ if line.startsWith(THEORY_TIMING_MARKER) && YXML.detect(line) => + case _ if Theory_Timing_Marker.test_yxml(line) => line match { case Theory_Timing(name, theory_timing) => theory_timings += (name -> (theory_timings.getOrElse(name, Map.empty) + theory_timing)) case _ => log_file.err("malformed theory_timing " + quote(line)) } - case _ if parse_ml_statistics && line.startsWith(ML_STATISTICS_MARKER) && YXML.detect(line) => - Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match { + case _ if parse_ml_statistics && ML_Statistics_Marker.test_yxml(line) => + ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match { case Some((SESSION_NAME, name) :: props) => ml_statistics += (name -> (props :: ml_statistics.getOrElse(name, Nil))) case _ => log_file.err("malformed ML_statistics " + quote(line)) } - case _ if line.startsWith(ERROR_MESSAGE_MARKER) && YXML.detect(line) => - Library.try_unprefix(ERROR_MESSAGE_MARKER, line).map(log_file.parse_props(_)) match { + case _ if Error_Message_Marker.test_yxml(line) => + Error_Message_Marker.unapply(line).map(log_file.parse_props) match { case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => - errors += (name -> (Library.decode_lines(msg) :: errors.getOrElse(name, Nil))) + errors += (name -> (msg :: errors.getOrElse(name, Nil))) case _ => log_file.err("malformed error message " + quote(line)) } @@ -663,12 +649,12 @@ task_statistics: Boolean): Session_Info = { Session_Info( - session_timing = log_file.find_props("\fTiming = ") getOrElse Nil, - command_timings = if (command_timings) log_file.filter_props("\fcommand_timing = ") else Nil, - theory_timings = if (theory_timings) log_file.filter_props(THEORY_TIMING_MARKER) else Nil, - ml_statistics = if (ml_statistics) log_file.filter_props(ML_STATISTICS_MARKER) else Nil, - task_statistics = if (task_statistics) log_file.filter_props("\ftask_statistics = ") else Nil, - errors = log_file.filter_lines(ERROR_MESSAGE_MARKER).map(Library.decode_lines(_))) + session_timing = log_file.find_props(Timing_Marker) getOrElse Nil, + command_timings = if (command_timings) log_file.filter_props(Command_Timing_Marker) else Nil, + theory_timings = if (theory_timings) log_file.filter_props(Theory_Timing_Marker) else Nil, + ml_statistics = if (ml_statistics) log_file.filter_props(ML_Statistics_Marker) else Nil, + task_statistics = if (task_statistics) log_file.filter_props(Task_Statistics_Marker) else Nil, + errors = log_file.filter(Error_Message_Marker)) } def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = diff -r e33f6e5f86b6 -r 5a4ccef7f310 src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Sun Mar 29 13:25:59 2020 +0200 +++ b/src/Pure/Admin/jenkins.scala Sun Mar 29 19:42:59 2020 +0200 @@ -112,7 +112,7 @@ File.write_xz(log_path, terminate_lines(Url.read(main_log) :: - ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _))), + ml_statistics.map(Build_Log.ML_Statistics_Marker.apply)), XZ.options(6)) } } diff -r e33f6e5f86b6 -r 5a4ccef7f310 src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala Sun Mar 29 13:25:59 2020 +0200 +++ b/src/Pure/PIDE/protocol_message.scala Sun Mar 29 19:42:59 2020 +0200 @@ -9,6 +9,32 @@ object Protocol_Message { + /* message markers */ + + object Marker + { + def apply(a: String): Marker = + new Marker { override def name: String = a } + } + + abstract class Marker private + { + def name: String + val prefix: String = "\f" + name + " = " + + def apply(text: String): String = prefix + Library.encode_lines(text) + def apply(props: Properties.T): String = apply(YXML.string_of_body(XML.Encode.properties(props))) + + def test(line: String): Boolean = line.startsWith(prefix) + def test_yxml(line: String): Boolean = test(line) && YXML.detect(line) + + def unapply(line: String): Option[String] = + Library.try_unprefix(prefix, line).map(Library.decode_lines) + + override def toString: String = "Marker(" + quote(name) + ")" + } + + /* inlined reports */ private val report_elements =