# HG changeset patch # User wenzelm # Date 1585562384 -7200 # Node ID 50425e4c3910d71a5ae0939093918d911a247369 # Parent 2e8f861d21d428562022bec7498b0a54f09279b2 clarified modules: global quasi-scope for markers; diff -r 2e8f861d21d4 -r 50425e4c3910 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Mon Mar 30 10:35:10 2020 +0200 +++ b/src/Pure/Admin/build_history.scala Mon Mar 30 11:59:44 2020 +0200 @@ -281,7 +281,7 @@ val theory_timings = try { store.read_theory_timings(db, session_name).map(ps => - Build_Log.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) + Protocol.Theory_Timing_Marker((Build_Log.SESSION_NAME, session_name) :: ps)) } catch { case ERROR(_) => Nil } @@ -355,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.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: + Protocol.Meta_Info_Marker(meta_info) :: build_result.out_lines ::: session_build_info ::: - ml_statistics.map(Build_Log.ML_Statistics_Marker.apply) ::: - session_errors.map(Build_Log.Error_Message_Marker.apply) ::: + ml_statistics.map(Protocol.ML_Statistics_Marker.apply) ::: + session_errors.map(Protocol.Error_Message_Marker.apply) ::: heap_sizes), XZ.options(6)) diff -r 2e8f861d21d4 -r 50425e4c3910 src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Mon Mar 30 10:35:10 2020 +0200 +++ b/src/Pure/Admin/build_log.scala Mon Mar 30 11:59:44 2020 +0200 @@ -387,8 +387,8 @@ } log_file.lines match { - 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 line :: _ if Protocol.Meta_Info_Marker.test_yxml(line) => + Meta_Info(log_file.find_props(Protocol.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, @@ -431,13 +431,6 @@ /** build info: toplevel output of isabelle build or Admin/build_history **/ - 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 @@ -503,7 +496,8 @@ object Theory_Timing { def unapply(line: String): Option[(String, (String, Timing))] = - Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match { + Protocol.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)) @@ -572,22 +566,22 @@ case Heap(name, Value.Long(size)) => heap_sizes += (name -> size) - case _ if Theory_Timing_Marker.test_yxml(line) => + case _ if Protocol.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 && ML_Statistics_Marker.test_yxml(line) => - ML_Statistics_Marker.unapply(line).map(log_file.parse_props) match { + case _ if parse_ml_statistics && Protocol.ML_Statistics_Marker.test_yxml(line) => + Protocol.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 Error_Message_Marker.test_yxml(line) => - Error_Message_Marker.unapply(line).map(log_file.parse_props) match { + case _ if Protocol.Error_Message_Marker.test_yxml(line) => + Protocol.Error_Message_Marker.unapply(line).map(log_file.parse_props) match { case Some(List((SESSION_NAME, name), (Markup.CONTENT, msg))) => errors += (name -> (msg :: errors.getOrElse(name, Nil))) case _ => log_file.err("malformed error message " + quote(line)) @@ -649,12 +643,16 @@ task_statistics: Boolean): Session_Info = { Session_Info( - 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)) + session_timing = log_file.find_props(Protocol.Timing_Marker) getOrElse Nil, + command_timings = + if (command_timings) log_file.filter_props(Protocol.Command_Timing_Marker) else Nil, + theory_timings = + if (theory_timings) log_file.filter_props(Protocol.Theory_Timing_Marker) else Nil, + ml_statistics = + if (ml_statistics) log_file.filter_props(Protocol.ML_Statistics_Marker) else Nil, + task_statistics = + if (task_statistics) log_file.filter_props(Protocol.Task_Statistics_Marker) else Nil, + errors = log_file.filter(Protocol.Error_Message_Marker)) } def compress_errors(errors: List[String], cache: XZ.Cache = XZ.cache()): Option[Bytes] = diff -r 2e8f861d21d4 -r 50425e4c3910 src/Pure/Admin/jenkins.scala --- a/src/Pure/Admin/jenkins.scala Mon Mar 30 10:35:10 2020 +0200 +++ b/src/Pure/Admin/jenkins.scala Mon Mar 30 11:59:44 2020 +0200 @@ -112,7 +112,7 @@ File.write_xz(log_path, terminate_lines(Url.read(main_log) :: - ml_statistics.map(Build_Log.ML_Statistics_Marker.apply)), + ml_statistics.map(Protocol.ML_Statistics_Marker.apply)), XZ.options(6)) } } diff -r 2e8f861d21d4 -r 50425e4c3910 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Mon Mar 30 10:35:10 2020 +0200 +++ b/src/Pure/PIDE/protocol.scala Mon Mar 30 11:59:44 2020 +0200 @@ -9,6 +9,19 @@ object Protocol { + /* markers for inlined messages */ + + val Loading_Theory_Marker = Protocol_Message.Marker("loading_theory") + val Export_Marker = Protocol_Message.Marker("export") + 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") + + /* document editing */ object Commands_Accepted @@ -161,8 +174,6 @@ /* export */ - val Export_Marker = Protocol_Message.Marker(Markup.EXPORT) - object Export { sealed case class Args( diff -r 2e8f861d21d4 -r 50425e4c3910 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Mon Mar 30 10:35:10 2020 +0200 +++ b/src/Pure/Tools/build.scala Mon Mar 30 11:59:44 2020 +0200 @@ -184,8 +184,6 @@ /* 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, @@ -294,7 +292,7 @@ process.result( progress_stdout = { - case Loading_Theory_Marker(theory) => + case Protocol.Loading_Theory_Marker(theory) => progress.theory(Progress.Theory(theory, session = name)) case Protocol.Export.Marker((args, path)) => val body =