# HG changeset patch # User wenzelm # Date 1585511860 -7200 # Node ID b3bddebe44caeb4f7cc87e5bc29a816fd3b9869d # Parent ab5009192ebb3db936e06329a46e0bb7df05e468 clarified signature: more explicit type Protocol_Message.Marker; diff -r ab5009192ebb -r b3bddebe44ca src/Pure/PIDE/markup.scala --- a/src/Pure/PIDE/markup.scala Sun Mar 29 21:32:20 2020 +0200 +++ b/src/Pure/PIDE/markup.scala Sun Mar 29 21:57:40 2020 +0200 @@ -625,6 +625,7 @@ /* export */ val EXPORT = "export" + val Export_Marker = Protocol_Message.Marker(EXPORT) object Export { @@ -645,25 +646,34 @@ val COMPRESS = "compress" val STRICT = "strict" - def dest_inline(props: Properties.T): Option[(Args, Path)] = + 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( + (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 + } + case _ => None + } + } + + def unapply(props: Properties.T): Option[Args] = 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)), diff -r ab5009192ebb -r b3bddebe44ca src/Pure/PIDE/protocol_message.scala --- a/src/Pure/PIDE/protocol_message.scala Sun Mar 29 21:32:20 2020 +0200 +++ b/src/Pure/PIDE/protocol_message.scala Sun Mar 29 21:57:40 2020 +0200 @@ -15,6 +15,8 @@ { def apply(a: String): Marker = new Marker { override def name: String = a } + + def test(line: String): Boolean = line.startsWith("\f") } abstract class Marker private diff -r ab5009192ebb -r b3bddebe44ca src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sun Mar 29 21:32:20 2020 +0200 +++ b/src/Pure/Tools/build.scala Sun Mar 29 21:57:40 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, @@ -291,24 +293,19 @@ process.result( progress_stdout = (line: String) => - Library.try_unprefix("\floading_theory = ", line) match { - case Some(theory) => + line match { + 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 Markup.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")