--- 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))
--- 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) {
--- 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))
}
}
--- 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;
--- 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 */
--- 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
--- 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 =
--- 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 =
--- 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)
--- 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);
--- 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] =
--- 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;
--- 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")