# HG changeset patch # User wenzelm # Date 1585513843 -7200 # Node ID 4c8edd527940d420360adffde9b761c93710a7ca # Parent a9de39608b1a887866f379b8dd05f893be10e3da# Parent 189f174792757e33c8d92681e16178e9d0ce2f3e merged diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Admin/build_history.scala Sun Mar 29 22:30:43 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 a9de39608b1a -r 4c8edd527940 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Admin/build_log.scala Sun Mar 29 22:30:43 2020 +0200 @@ -103,7 +103,7 @@ def plain_name(name: String): String = { - List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith(_)) match { + List(".log", ".log.gz", ".log.xz", ".gz", ".xz").find(name.endsWith) match { case Some(s) => Library.try_unsuffix(s, name).get case None => name } @@ -138,8 +138,8 @@ { val name = file.getName - prefixes.exists(name.startsWith(_)) && - suffixes.exists(name.endsWith(_)) && + prefixes.exists(name.startsWith) && + suffixes.exists(name.endsWith) && name != "isatest.log" && name != "afp-test.log" && name != "main.log" @@ -179,20 +179,14 @@ def tune(s: String): String = Word.implode( Word.explode(s) match { - case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone(_)) - case a :: bs => tune_weekday(a) :: bs.map(tune_timezone(_)) + case a :: "M\uFFFDr" :: bs => tune_weekday(a) :: "Mär" :: bs.map(tune_timezone) + case a :: bs => tune_weekday(a) :: bs.map(tune_timezone) case Nil => Nil } ) 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 */ @@ -304,7 +290,7 @@ Properties.get(settings, c.name) def get_date(c: SQL.Column): Option[Date] = - get(c).map(Log_File.Date_Format.parse(_)) + get(c).map(Log_File.Date_Format.parse) } object Identify @@ -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] = @@ -681,7 +667,7 @@ def uncompress_errors(bytes: Bytes, cache: XZ.Cache = XZ.cache()): List[String] = if (bytes.isEmpty) Nil else { - XML.Decode.list(YXML.string_of_body(_))(YXML.parse_body(bytes.uncompress(cache = cache).text)) + XML.Decode.list(YXML.string_of_body)(YXML.parse_body(bytes.uncompress(cache = cache).text)) } @@ -754,7 +740,7 @@ /* earliest pull date for repository version (PostgreSQL queries) */ - def pull_date(afp: Boolean = false) = + def pull_date(afp: Boolean = false): SQL.Column = if (afp) SQL.Column.date("afp_pull_date") else SQL.Column.date("pull_date") @@ -1110,7 +1096,7 @@ files.filter(file => status.exists(_.required(file))). grouped(options.int("build_log_transaction_size") max 1)) { - val log_files = Par_List.map[JFile, Log_File](Log_File.apply _, file_group) + val log_files = Par_List.map[JFile, Log_File](Log_File.apply, file_group) db.transaction { log_files.foreach(log_file => status.foreach(_.update(log_file))) } } } @@ -1182,7 +1168,7 @@ res.timing(Data.ml_timing_elapsed, Data.ml_timing_cpu, Data.ml_timing_gc), sources = res.get_string(Data.sources), heap_size = res.get_long(Data.heap_size), - status = res.get_string(Data.status).map(Session_Status.withName(_)), + status = res.get_string(Data.status).map(Session_Status.withName), errors = uncompress_errors(res.bytes(Data.errors), cache = xz_cache), ml_statistics = if (ml_statistics) { diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Admin/jenkins.scala Sun Mar 29 22:30:43 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 a9de39608b1a -r 4c8edd527940 src/Pure/General/output_primitives.ML --- a/src/Pure/General/output_primitives.ML Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/General/output_primitives.ML Sun Mar 29 22:30:43 2020 +0200 @@ -49,6 +49,7 @@ | Text of string; type body = tree list; + end; diff -r a9de39608b1a -r 4c8edd527940 src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/PIDE/markup.scala Sun Mar 29 22:30:43 2020 +0200 @@ -625,57 +625,10 @@ /* export */ val EXPORT = "export" - - object Export - { - sealed case class Args( - id: Option[String], - serial: Long, - theory_name: String, - name: String, - executable: Boolean, - compress: Boolean, - strict: Boolean) - { - def compound_name: String = isabelle.Export.compound_name(theory_name, name) - } - - val THEORY_NAME = "theory_name" - val EXECUTABLE = "executable" - val COMPRESS = "compress" - val STRICT = "strict" - - def dest_inline(props: Properties.T): Option[(Args, Path)] = - props match { - case - List( - (SERIAL, Value.Long(serial)), - (THEORY_NAME, theory_name), - (NAME, name), - (EXECUTABLE, Value.Boolean(executable)), - (COMPRESS, Value.Boolean(compress)), - (STRICT, Value.Boolean(strict)), - (FILE, file)) if isabelle.Path.is_valid(file) => - val args = Args(None, serial, theory_name, name, executable, compress, strict) - Some((args, isabelle.Path.explode(file))) - case _ => None - } - - def unapply(props: Properties.T): Option[Args] = - props match { - case List( - (FUNCTION, EXPORT), - (ID, id), - (SERIAL, Value.Long(serial)), - (THEORY_NAME, theory_name), - (NAME, name), - (EXECUTABLE, Value.Boolean(executable)), - (COMPRESS, Value.Boolean(compress)), - (STRICT, Value.Boolean(strict))) => - Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) - case _ => None - } - } + val THEORY_NAME = "theory_name" + val EXECUTABLE = "executable" + val COMPRESS = "compress" + val STRICT = "strict" /* debugger output */ diff -r a9de39608b1a -r 4c8edd527940 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/PIDE/protocol.scala Sun Mar 29 22:30:43 2020 +0200 @@ -159,6 +159,66 @@ } + /* export */ + + val Export_Marker = Protocol_Message.Marker(Markup.EXPORT) + + object Export + { + sealed case class Args( + id: Option[String], + serial: Long, + theory_name: String, + name: String, + executable: Boolean, + compress: Boolean, + strict: Boolean) + { + def compound_name: String = isabelle.Export.compound_name(theory_name, name) + } + + object Marker + { + def unapply(line: String): Option[(Args, Path)] = + line match { + case Export_Marker(text) => + val props = XML.Decode.properties(YXML.parse_body(text)) + props match { + case + List( + (Markup.SERIAL, Value.Long(serial)), + (Markup.THEORY_NAME, theory_name), + (Markup.NAME, name), + (Markup.EXECUTABLE, Value.Boolean(executable)), + (Markup.COMPRESS, Value.Boolean(compress)), + (Markup.STRICT, Value.Boolean(strict)), + (Markup.FILE, file)) if isabelle.Path.is_valid(file) => + val args = Args(None, serial, theory_name, name, executable, compress, strict) + Some((args, isabelle.Path.explode(file))) + case _ => None + } + case _ => None + } + } + + def unapply(props: Properties.T): Option[Args] = + props match { + case + List( + (Markup.FUNCTION, Markup.EXPORT), + (Markup.ID, id), + (Markup.SERIAL, Value.Long(serial)), + (Markup.THEORY_NAME, theory_name), + (Markup.NAME, name), + (Markup.EXECUTABLE, Value.Boolean(executable)), + (Markup.COMPRESS, Value.Boolean(compress)), + (Markup.STRICT, Value.Boolean(strict))) => + Some(Args(proper_string(id), serial, theory_name, name, executable, compress, strict)) + case _ => None + } + } + + /* breakpoints */ object ML_Breakpoint diff -r a9de39608b1a -r 4c8edd527940 src/Pure/PIDE/protocol_message.ML --- a/src/Pure/PIDE/protocol_message.ML Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/PIDE/protocol_message.ML Sun Mar 29 22:30:43 2020 +0200 @@ -6,7 +6,8 @@ signature PROTOCOL_MESSAGE = sig - val inline: string -> Properties.T -> unit + val marker_text: string -> string -> unit + val marker: string -> Properties.T -> unit val command_positions: string -> XML.body -> XML.body val command_positions_yxml: string -> string -> string end; @@ -14,8 +15,11 @@ structure Protocol_Message: PROTOCOL_MESSAGE = struct -fun inline a args = - writeln ("\f" ^ a ^ " = " ^ YXML.string_of_body (XML.Encode.properties args)); +fun marker_text a text = + Output.physical_writeln ("\f" ^ a ^ " = " ^ encode_lines text); + +fun marker a props = + marker_text a (YXML.string_of_body (XML.Encode.properties props)); fun command_positions id = diff -r a9de39608b1a -r 4c8edd527940 src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/PIDE/protocol_message.scala Sun Mar 29 22:30:43 2020 +0200 @@ -9,6 +9,34 @@ object Protocol_Message { + /* message markers */ + + object Marker + { + def apply(a: String): Marker = + new Marker { override def name: String = a } + + def test(line: String): Boolean = line.startsWith("\f") + } + + 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 = diff -r a9de39608b1a -r 4c8edd527940 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/PIDE/session.scala Sun Mar 29 22:30:43 2020 +0200 @@ -486,7 +486,7 @@ case Protocol.Theory_Timing(_, _) => // FIXME - case Markup.Export(args) + case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => val id = Value.Long.unapply(args.id.get).get val export = Export.make_entry("", args, msg.bytes, cache = xz_cache) diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Thy/export.ML --- a/src/Pure/Thy/export.ML Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Thy/export.ML Sun Mar 29 22:30:43 2020 +0200 @@ -83,7 +83,7 @@ let val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ())); val _ = YXML.write_body path body; - in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end + in Protocol_Message.marker (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end else raise Output.Protocol_Message props | [] => raise Output.Protocol_Message props); diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Thy/export.scala --- a/src/Pure/Thy/export.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Thy/export.scala Sun Mar 29 22:30:43 2020 +0200 @@ -143,7 +143,7 @@ regex.pattern.matcher(compound_name(theory_name, name)).matches } - def make_entry(session_name: String, args: Markup.Export.Args, body: Bytes, + def make_entry(session_name: String, args: Protocol.Export.Args, body: Bytes, cache: XZ.Cache = XZ.cache()): Entry = { Entry(session_name, args.theory_name, args.name, args.executable, @@ -213,7 +213,7 @@ (results, true) }) - def apply(session_name: String, args: Markup.Export.Args, body: Bytes): Unit = + def apply(session_name: String, args: Protocol.Export.Args, body: Bytes): Unit = consumer.send(make_entry(session_name, args, body, cache = cache) -> args.strict) def shutdown(close: Boolean = false): List[String] = diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Tools/build.ML --- a/src/Pure/Tools/build.ML Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Tools/build.ML Sun Mar 29 22:30:43 2020 +0200 @@ -58,7 +58,7 @@ val timing_props = [("threads", threads)] @ Markup.timing_properties timing @ [("factor", factor)]; - val _ = writeln ("\fTiming = " ^ YXML.string_of_body (XML.Encode.properties timing_props)); + val _ = Protocol_Message.marker "Timing" timing_props; val _ = if verbose then Output.physical_stderr ("Timing " ^ name ^ " (" ^ @@ -73,7 +73,7 @@ (case props of function :: args => if function = Markup.ML_statistics orelse function = Markup.task_statistics then - Protocol_Message.inline (#2 function) args + Protocol_Message.marker (#2 function) args else if function = Markup.command_timing then let val name = the_default "" (Properties.get args Markup.nameN); @@ -86,15 +86,16 @@ if is_significant then (case approximative_id name pos of SOME id => - Protocol_Message.inline (#2 function) (Markup.command_timing_properties id elapsed) + Protocol_Message.marker (#2 function) + (Markup.command_timing_properties id elapsed) | NONE => ()) else () end else if function = Markup.theory_timing then - Protocol_Message.inline (#2 function) args + Protocol_Message.marker (#2 function) args else (case Markup.dest_loading_theory props of - SOME name => writeln ("\floading_theory = " ^ name) + SOME name => Protocol_Message.marker_text "loading_theory" name | NONE => Export.protocol_message props output) | [] => raise Output.Protocol_Message props); @@ -219,6 +220,10 @@ if name = Context.PureN then Theory.install_pure (Thy_Info.get_theory Context.PureN) else (); in () end; +fun inline_errors exn = + Runtime.exn_message_list exn + |> List.app (fn msg => Protocol_Message.marker_text "error_message" (YXML.content_of msg)); + (*command-line tool*) fun build args_file = let @@ -226,11 +231,10 @@ val _ = Options.load_default (); val _ = Isabelle_Process.init_options (); val args = decode_args (File.read (Path.explode args_file)); - fun error_message msg = writeln ("\ferror_message = " ^ encode_lines (YXML.content_of msg)); val _ = Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message build_session args - handle exn => (List.app error_message (Runtime.exn_message_list exn); Exn.reraise exn); + handle exn => (inline_errors exn; Exn.reraise exn); val _ = Private_Output.protocol_message_fn := Output.protocol_message_undefined; val _ = Options.reset_default (); in () end; diff -r a9de39608b1a -r 4c8edd527940 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Mar 29 15:44:54 2020 +0100 +++ b/src/Pure/Tools/build.scala Sun Mar 29 22:30:43 2020 +0200 @@ -184,6 +184,8 @@ /* job: running prover process */ + private val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") + private class Job(progress: Progress, name: String, val info: Sessions.Info, @@ -290,25 +292,20 @@ } process.result( - progress_stdout = (line: String) => - Library.try_unprefix("\floading_theory = ", line) match { - case Some(theory) => + progress_stdout = + { + case Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, session = name)) - case None => - for { - text <- Library.try_unprefix("\fexport = ", line) - (args, path) <- - Markup.Export.dest_inline(XML.Decode.properties(YXML.parse_body(text))) - } { - val body = - try { Bytes.read(path) } - catch { - case ERROR(msg) => - error("Failed to read export " + quote(args.compound_name) + "\n" + msg) - } - path.file.delete - export_consumer(name, args, body) - } + case Protocol.Export.Marker((args, path)) => + val body = + try { Bytes.read(path) } + catch { + case ERROR(msg) => + error("Failed to read export " + quote(args.compound_name) + "\n" + msg) + } + path.file.delete + export_consumer(name, args, body) + case _ => }, progress_limit = options.int("process_output_limit") match { @@ -540,7 +537,7 @@ val (process_result, heap_digest) = job.join - val log_lines = process_result.out_lines.filterNot(_.startsWith("\f")) + val log_lines = process_result.out_lines.filterNot(Protocol_Message.Marker.test) val process_result_tail = { val tail = job.info.options.int("process_output_tail")