# HG changeset patch # User wenzelm # Date 1585775068 -7200 # Node ID 0aef1812ae3a51d0db12672dd1c7abb33123e802 # Parent 9d8fb1dbc3689b23469aec52bf7dea8edfe93afc# Parent 6f7a54954f19a5e5e83ad52c2b0aacd1fabf2376 merged diff -r 9d8fb1dbc368 -r 0aef1812ae3a etc/options --- a/etc/options Wed Apr 01 21:48:39 2020 +0200 +++ b/etc/options Wed Apr 01 23:04:28 2020 +0200 @@ -123,6 +123,9 @@ option system_heaps : bool = false -- "store session heaps in $ISABELLE_HEAPS_SYSTEM, not $ISABELLE_HEAPS" +option pide_build : bool = false + -- "build session heaps via PIDE" + section "ML System" diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/Admin/build_log.scala Wed Apr 01 23:04:28 2020 +0200 @@ -110,10 +110,10 @@ } def apply(name: String, lines: List[String]): Log_File = - new Log_File(plain_name(name), lines) + new Log_File(plain_name(name), lines.map(Library.trim_line)) def apply(name: String, text: String): Log_File = - Log_File(name, Library.trim_split_lines(text)) + new Log_File(plain_name(name), Library.trim_split_lines(text)) def apply(file: JFile): Log_File = { diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/General/output.ML --- a/src/Pure/General/output.ML Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/General/output.ML Wed Apr 01 23:04:28 2020 +0200 @@ -59,7 +59,6 @@ val report_fn: (output list -> unit) Unsynchronized.ref val result_fn: (Properties.T -> output list -> unit) Unsynchronized.ref val protocol_message_fn: Output_Primitives.protocol_message_fn Unsynchronized.ref - val init_channels: unit -> unit end; structure Private_Output: PRIVATE_OUTPUT = diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/General/output.scala --- a/src/Pure/General/output.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/General/output.scala Wed Apr 01 23:04:28 2020 +0200 @@ -15,11 +15,11 @@ def writeln_text(msg: String): String = clean_yxml(msg) - def warning_text(msg: String): String = - Library.prefix_lines("### ", clean_yxml(msg)) + def warning_prefix(s: String): String = Library.prefix_lines("### ", s) + def warning_text(msg: String): String = warning_prefix(clean_yxml(msg)) - def error_message_text(msg: String): String = - Library.prefix_lines("*** ", clean_yxml(msg)) + def error_prefix(s: String): String = Library.prefix_lines("*** ", s) + def error_message_text(msg: String): String = error_prefix(clean_yxml(msg)) def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false) { diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/General/symbol.ML Wed Apr 01 23:04:28 2020 +0200 @@ -501,10 +501,9 @@ (* length *) fun sym_len s = - if not (is_printable s) then (0: int) - else if String.isPrefix "\092 fn n => sym_len s + n) ss 0; diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/General/symbol.scala Wed Apr 01 23:04:28 2020 +0200 @@ -23,6 +23,7 @@ /* spaces */ + val space_char = ' ' val space = " " private val static_spaces = space * 4000 @@ -37,6 +38,8 @@ /* ASCII characters */ + def is_ascii_printable(c: Char): Boolean = space_char <= c && c <= '~' + def is_ascii_letter(c: Char): Boolean = 'A' <= c && c <= 'Z' || 'a' <= c && c <= 'z' def is_ascii_digit(c: Char): Boolean = '0' <= c && c <= '9' @@ -654,4 +657,23 @@ def esub_decoded: Symbol = symbols.esub_decoded def bsup_decoded: Symbol = symbols.bsup_decoded def esup_decoded: Symbol = symbols.esup_decoded + + + /* metric */ + + def is_printable(sym: Symbol): Boolean = + if (is_ascii(sym)) is_ascii_printable(sym(0)) + else !is_control(sym) + + object Metric extends Pretty.Metric + { + val unit = 1.0 + def apply(str: String): Double = + (for (s <- iterator(str)) yield { + val sym = encode(s) + if (sym.startsWith("\\ List("--eval", eval)) ::: args + (eval_init ::: eval_modes ::: eval_options ::: eval_session_base).flatMap(List("--eval", _)) ::: + use_prelude.flatMap(List("--use", _)) ::: List("--eval", eval_process) ::: args Bash.process( "exec " + options.string("ML_process_policy") + """ "$ML_HOME/poly" -q """ + diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/PIDE/protocol.scala Wed Apr 01 23:04:28 2020 +0200 @@ -102,6 +102,12 @@ /* result messages */ + def is_message(pred: XML.Elem => Boolean, body: XML.Body): Boolean = + body match { + case List(elem: XML.Elem) => pred(elem) + case _ => false + } + def is_result(msg: XML.Tree): Boolean = msg match { case XML.Elem(Markup(Markup.RESULT, _), _) => true @@ -163,11 +169,17 @@ def is_exported(msg: XML.Tree): Boolean = is_writeln(msg) || is_warning(msg) || is_legacy(msg) || is_error(msg) - def message_text(msg: XML.Tree): String = + def message_text(body: XML.Body, + margin: Double = Pretty.default_margin, + breakgain: Double = Pretty.default_breakgain, + metric: Pretty.Metric = Pretty.Default_Metric): String = { - val text = Pretty.string_of(List(msg)) - if (is_warning(msg) || is_legacy(msg)) Library.prefix_lines("### ", text) - else if (is_error(msg)) Library.prefix_lines("*** ", text) + val text = + Pretty.string_of(Protocol_Message.expose_no_reports(body), + margin = margin, breakgain = breakgain, metric = metric) + + if (is_message(is_warning, body) || is_message(is_legacy, body)) Output.warning_prefix(text) + else if (is_message(is_error, body)) Output.error_prefix(text) else text } diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/PIDE/prover.scala --- a/src/Pure/PIDE/prover.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/PIDE/prover.scala Wed Apr 01 23:04:28 2020 +0200 @@ -45,7 +45,7 @@ { val res = if (is_status || is_report) message.body.map(_.toString).mkString - else Pretty.string_of(message.body) + else Pretty.string_of(message.body, metric = Symbol.Metric) if (properties.isEmpty) kind.toString + " [[" + res + "]]" else @@ -114,6 +114,8 @@ private val process_manager = Standard_Thread.fork("process_manager") { + val stdout = physical_output(false) + val (startup_failed, startup_errors) = { var finished: Option[Boolean] = None @@ -127,7 +129,7 @@ } catch { case _: IOException => finished = Some(false) } } - Thread.sleep(10) + Thread.sleep(50) } (finished.isEmpty || !finished.get, result.toString.trim) } @@ -136,13 +138,13 @@ if (startup_failed) { terminate_process() process_result.join + stdout.join exit_message(Process_Result(127)) } else { val (command_stream, message_stream) = channel.rendezvous() command_input_init(command_stream) - val stdout = physical_output(false) val stderr = physical_output(true) val message = message_output(message_stream) diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/PIDE/session.scala Wed Apr 01 23:04:28 2020 +0200 @@ -61,7 +61,10 @@ /* events */ //{{{ - case class Statistics(props: Properties.T) + case class Command_Timing(props: Properties.T) + case class Theory_Timing(props: Properties.T) + case class Runtime_Statistics(props: Properties.T) + case class Task_Statistics(props: Properties.T) case class Global_Options(options: Options) case object Caret_Focus case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) @@ -175,7 +178,10 @@ /* outlets */ - val statistics = new Session.Outlet[Session.Statistics](dispatcher) + val command_timings = new Session.Outlet[Session.Command_Timing](dispatcher) + val theory_timings = new Session.Outlet[Session.Theory_Timing](dispatcher) + val runtime_statistics = new Session.Outlet[Session.Runtime_Statistics](dispatcher) + val task_statistics = new Session.Outlet[Session.Task_Statistics](dispatcher) val global_options = new Session.Outlet[Session.Global_Options](dispatcher) val caret_focus = new Session.Outlet[Session.Caret_Focus.type](dispatcher) val raw_edits = new Session.Outlet[Session.Raw_Edits](dispatcher) @@ -480,11 +486,12 @@ init_protocol_handler(name) case Protocol.Command_Timing(state_id, timing) if prover.defined => + command_timings.post(Session.Command_Timing(msg.properties)) val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) change_command(_.accumulate(state_id, xml_cache.elem(message), xml_cache)) case Protocol.Theory_Timing(_, _) => - // FIXME + theory_timings.post(Session.Theory_Timing(msg.properties)) case Protocol.Export(args) if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => @@ -526,10 +533,10 @@ } case Markup.ML_Statistics(props) => - statistics.post(Session.Statistics(props)) + runtime_statistics.post(Session.Runtime_Statistics(props)) case Markup.Task_Statistics(props) => - // FIXME + task_statistics.post(Session.Task_Statistics(props)) case _ => bad_output() } diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/System/isabelle_process.ML --- a/src/Pure/System/isabelle_process.ML Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/System/isabelle_process.ML Wed Apr 01 23:04:28 2020 +0200 @@ -14,6 +14,7 @@ val init_options: unit -> unit val init_options_interactive: unit -> unit val init: unit -> unit + val init_build: unit -> unit end; structure Isabelle_Process: ISABELLE_PROCESS = @@ -28,6 +29,9 @@ val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape; val _ = Markup.add_mode isabelle_processN YXML.output_markup; +val protocol_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; +val protocol_modes2 = [isabelle_processN, Pretty.symbolicN]; + (* protocol commands *) @@ -92,16 +96,41 @@ end); -(* output channels *) +(* init protocol -- uninterruptible *) + +exception EXIT of exn; + +val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); + +local + +fun recover crash = + (Synchronized.change crashes (cons crash); + Output.physical_stderr + "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); -val serial_props = Markup.serial_properties o serial; +in + +fun init_protocol modes = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => + let + val _ = SHA1.test_samples () + handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); -fun init_channels out_stream = - let + val _ = Output.physical_stderr Symbol.STX; + + + (* streams *) + + val (in_stream, out_stream) = Socket_IO.open_streams address; + val _ = Byte_Message.write_line out_stream password; + val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdOut, IO.LINE_BUF); val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream TextIO.stdErr, IO.LINE_BUF); val _ = BinIO.StreamIO.setBufferMode (BinIO.getOutstream out_stream, IO.BLOCK_BUF); + + (* messages *) + val msg_channel = Message_Channel.make out_stream; fun message name props body = @@ -116,90 +145,72 @@ (false, SOME id') => props @ [(Markup.idN, id')] | _ => props); in message name props' (XML.blob ss) end; - in - Private_Output.status_fn := standard_message [] Markup.statusN; - Private_Output.report_fn := standard_message [] Markup.reportN; - Private_Output.result_fn := - (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s); - Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s); - Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s); - Private_Output.information_fn := - (fn s => standard_message (serial_props ()) Markup.informationN s); - Private_Output.tracing_fn := - (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)); - Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s); - Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s); - Private_Output.error_message_fn := - (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s); - Private_Output.system_message_fn := - (fn ss => message Markup.systemN [] (XML.blob ss)); - Private_Output.protocol_message_fn := - (fn props => fn body => message Markup.protocolN props body); + + val serial_props = Markup.serial_properties o serial; - Session.init_protocol_handlers (); - message Markup.initN [] [XML.Text (Session.welcome ())]; - msg_channel - end; + val message_context = + Unsynchronized.setmp Private_Output.status_fn + (standard_message [] Markup.statusN) #> + Unsynchronized.setmp Private_Output.report_fn + (standard_message [] Markup.reportN) #> + Unsynchronized.setmp Private_Output.result_fn + (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s) #> + Unsynchronized.setmp Private_Output.writeln_fn + (fn s => standard_message (serial_props ()) Markup.writelnN s) #> + Unsynchronized.setmp Private_Output.state_fn + (fn s => standard_message (serial_props ()) Markup.stateN s) #> + Unsynchronized.setmp Private_Output.information_fn + (fn s => standard_message (serial_props ()) Markup.informationN s) #> + Unsynchronized.setmp Private_Output.tracing_fn + (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s)) #> + Unsynchronized.setmp Private_Output.warning_fn + (fn s => standard_message (serial_props ()) Markup.warningN s) #> + Unsynchronized.setmp Private_Output.legacy_fn + (fn s => standard_message (serial_props ()) Markup.legacyN s) #> + Unsynchronized.setmp Private_Output.error_message_fn + (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s) #> + Unsynchronized.setmp Private_Output.system_message_fn + (fn ss => message Markup.systemN [] (XML.blob ss)) #> + Unsynchronized.setmp Private_Output.protocol_message_fn + (fn props => fn body => message Markup.protocolN props body) #> + Unsynchronized.setmp print_mode + ((! print_mode @ #1 modes) |> fold (update op =) (#2 modes)); -(* protocol loop -- uninterruptible *) - -exception EXIT of exn; - -val crashes = Synchronized.var "Isabelle_Process.crashes" ([]: exn list); + (* protocol *) -local - -fun recover crash = - (Synchronized.change crashes (cons crash); - Output.physical_stderr - "Recovered from Isabelle process crash -- see also Isabelle_Process.crashes\n"); + fun protocol_loop () = + let + val continue = + (case Byte_Message.read_message in_stream of + NONE => false + | SOME [] => (Output.system_message "Isabelle process: no input"; true) + | SOME (name :: args) => (run_command name args; true)) + handle EXIT exn => Exn.reraise exn + | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); + in if continue then protocol_loop () else () end; -fun shutdown () = (Future.shutdown (); ignore (Execution.reset ())); + fun protocol () = + (Session.init_protocol_handlers (); + message Markup.initN [] [XML.Text (Session.welcome ())]; + protocol_loop ()); -in + val result = Exn.capture (message_context protocol) (); + -fun loop stream = - let - val continue = - (case Byte_Message.read_message stream of - NONE => false - | SOME [] => (Output.system_message "Isabelle process: no input"; true) - | SOME (name :: args) => (run_command name args; true)) - handle EXIT exn => (shutdown (); Exn.reraise exn) - | exn => (Runtime.exn_system_message exn handle crash => recover crash; true); - in if continue then loop stream else shutdown () end; + (* shutdown *) + + val _ = Future.shutdown (); + val _ = Execution.reset (); + val _ = Message_Channel.shutdown msg_channel; + val _ = BinIO.closeIn in_stream; + val _ = BinIO.closeOut out_stream; + + in Exn.release result end); end; -(* init protocol *) - -val default_modes1 = [Syntax_Trans.no_bracketsN, Syntax_Trans.no_type_bracketsN]; -val default_modes2 = [isabelle_processN, Pretty.symbolicN]; - -val init_protocol = Thread_Attributes.uninterruptible (fn _ => fn (address, password) => - let - val _ = SHA1.test_samples () - handle exn as Fail msg => (Output.physical_stderr (msg ^ "\n"); Exn.reraise exn); - val _ = Output.physical_stderr Symbol.STX; - - val _ = Context.put_generic_context NONE; - val _ = - Unsynchronized.change print_mode - (fn mode => (mode @ default_modes1) |> fold (update op =) default_modes2); - - val (in_stream, out_stream) = Socket_IO.open_streams address; - val _ = Byte_Message.write_line out_stream password; - val msg_channel = init_channels out_stream; - val _ = loop in_stream; - val _ = Message_Channel.shutdown msg_channel; - val _ = Private_Output.init_channels (); - - val _ = print_mode := []; - in () end); - - (* init options *) fun init_options () = @@ -221,14 +232,17 @@ (* generic init *) -fun init () = +fun init_modes modes = let val address = Options.default_string \<^system_option>\system_channel_address\; val password = Options.default_string \<^system_option>\system_channel_password\; in if address <> "" andalso password <> "" - then init_protocol (address, password) + then init_protocol modes (address, password) else init_options () end; +fun init () = init_modes (protocol_modes1, protocol_modes2); +fun init_build () = init_modes ([], protocol_modes2); + end; diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/System/isabelle_process.scala Wed Apr 01 23:04:28 2020 +0200 @@ -18,7 +18,9 @@ sessions_structure: Sessions.Structure, store: Sessions.Store, logic: String = "", - args: List[String] = Nil, + raw_ml_system: Boolean = false, + use_prelude: List[String] = Nil, + eval_main: String = "", modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings()): Isabelle_Process = @@ -30,7 +32,9 @@ options.string.update("system_channel_address", channel.address). string.update("system_channel_password", channel.password) ML_Process(channel_options, sessions_structure, store, - logic = logic, args = args, modes = modes, cwd = cwd, env = env) + logic = logic, raw_ml_system = raw_ml_system, + use_prelude = use_prelude, eval_main = eval_main, + modes = modes, cwd = cwd, env = env) } catch { case exn @ ERROR(_) => channel.shutdown(); throw exn } process.stdin.close diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/System/process_result.scala --- a/src/Pure/System/process_result.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/System/process_result.scala Wed Apr 01 23:04:28 2020 +0200 @@ -16,8 +16,10 @@ def out: String = cat_lines(out_lines) def err: String = cat_lines(err_lines) - def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs) - def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs) + def output(outs: List[String]): Process_Result = + copy(out_lines = out_lines ::: outs.flatMap(split_lines)) + def errors(errs: List[String]): Process_Result = + copy(err_lines = err_lines ::: errs.flatMap(split_lines)) def error(err: String): Process_Result = errors(List(err)) def was_timeout: Process_Result = copy(rc = 1, timeout = true) diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/Thy/sessions.scala Wed Apr 01 23:04:28 2020 +0200 @@ -143,21 +143,19 @@ val doc_names = Doc.doc_names() + val bootstrap = + Sessions.Base.bootstrap( + sessions_structure.session_directories, + sessions_structure.global_theories) + val session_bases = - (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({ + (Map("" -> bootstrap) /: sessions_structure.imports_topological_order)({ case (session_bases, session_name) => progress.expose_interrupt() val info = sessions_structure(session_name) try { - val parent_base: Sessions.Base = - info.parent match { - case None => - Base.bootstrap( - sessions_structure.session_directories, - sessions_structure.global_theories) - case Some(parent) => session_bases(parent) - } + val parent_base = session_bases(info.parent.getOrElse("")) val imports_base: Sessions.Base = { diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/Tools/build.scala Wed Apr 01 23:04:28 2020 +0200 @@ -8,7 +8,7 @@ package isabelle -import scala.collection.SortedSet +import scala.collection.{SortedSet, mutable} import scala.annotation.tailrec @@ -161,8 +161,8 @@ { val errors = try { - XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text)). - map(err => Pretty.string_of(Protocol_Message.expose_no_reports(err))) + for (err <- XML.Decode.list(x => x)(Symbol.decode_yxml(msg.text))) yield + Pretty.string_of(Protocol_Message.expose_no_reports(err), metric = Symbol.Metric) } catch { case ERROR(err) => List(err) } build_session_errors.fulfill(errors) @@ -194,7 +194,6 @@ store: Sessions.Store, do_store: Boolean, verbose: Boolean, - pide: Boolean, val numa_node: Option[Int], command_timings: List[Properties.T]) { @@ -212,7 +211,7 @@ private val future_result: Future[Process_Result] = Future.thread("build") { val parent = info.parent.getOrElse("") - val base = deps(name) + val base = deps(parent) val args_yxml = YXML.string_of_body( { @@ -242,27 +241,72 @@ val is_pure = Sessions.is_pure(name) + val use_prelude = if (is_pure) Thy_Header.ml_roots.map(_._1) else Nil + val eval_store = - if (!do_store) Nil - else { + if (do_store) { (if (info.theories.nonEmpty) List("ML_Heap.share_common_data ()") else Nil) ::: List("ML_Heap.save_child " + ML_Syntax.print_string_bytes(File.platform_path(store.output_heap(name)))) } + else Nil - if (pide && !is_pure) { + if (options.bool("pide_build")) { val resources = new Resources(sessions_structure, deps(parent)) val session = new Session(options, resources) val handler = new Handler(progress, session, name) session.init_protocol_handler(handler) + val stdout = new StringBuilder(1000) + val messages = new mutable.ListBuffer[String] + val command_timings = new mutable.ListBuffer[Properties.T] + val theory_timings = new mutable.ListBuffer[Properties.T] + val runtime_statistics = new mutable.ListBuffer[Properties.T] + val task_statistics = new mutable.ListBuffer[Properties.T] + + val consumer = + Session.Consumer[Any]("build_session_output") { + case msg: Prover.Output => + val message = msg.message + if (msg.is_stdout) { + stdout ++= Symbol.encode(XML.content(message)) + } + else if (Protocol.is_exported(message)) { + messages += + Symbol.encode(Protocol.message_text(List(message), metric = Symbol.Metric)) + } + case Session.Command_Timing(props) => command_timings += props + case Session.Theory_Timing(props) => theory_timings += props + case Session.Runtime_Statistics(props) => runtime_statistics += props + case Session.Task_Statistics(props) => task_statistics += props + case _ => + } + + session.all_messages += consumer + session.command_timings += consumer + session.theory_timings += consumer + session.runtime_statistics += consumer + session.task_statistics += consumer + + val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) + val process = Isabelle_Process(session, options, sessions_structure, store, - logic = parent, cwd = info.dir.file, env = env).await_startup + logic = parent, raw_ml_system = is_pure, + use_prelude = use_prelude, eval_main = eval_main, + cwd = info.dir.file, env = env).await_startup session.protocol_command("build_session", args_yxml) - val result = process.join + val process_result = process.join + val process_output = + stdout.toString :: messages.toList ::: + command_timings.toList.map(Protocol.Command_Timing_Marker.apply) ::: + theory_timings.toList.map(Protocol.Theory_Timing_Marker.apply) ::: + runtime_statistics.toList.map(Protocol.ML_Statistics_Marker.apply) ::: + task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) + + val result = process_result.output(process_output) handler.build_session_errors.join match { case Nil => result case errors => @@ -275,22 +319,15 @@ val args_file = Isabelle_System.tmp_file("build") File.write(args_file, args_yxml) - val eval_build = "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) - val eval = Command_Line.ML_tool(eval_build :: eval_store) + val eval_build = + "Build.build " + ML_Syntax.print_string_bytes(File.standard_path(args_file)) + val eval_main = Command_Line.ML_tool(eval_build :: eval_store) val process = - if (is_pure) { - ML_Process(options, deps.sessions_structure, store, raw_ml_system = true, - args = - (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten ::: - List("--eval", eval), - cwd = info.dir.file, env = env, cleanup = () => args_file.delete) - } - else { - ML_Process(options, deps.sessions_structure, store, logic = parent, - args = List("--eval", eval), - cwd = info.dir.file, env = env, cleanup = () => args_file.delete) - } + ML_Process(options, deps.sessions_structure, store, + logic = parent, raw_ml_system = is_pure, + use_prelude = use_prelude, eval_main = eval_main, + cwd = info.dir.file, env = env, cleanup = () => args_file.delete) process.result( progress_stdout = @@ -401,7 +438,6 @@ soft_build: Boolean = false, verbose: Boolean = false, export_files: Boolean = false, - pide: Boolean = false, requirements: Boolean = false, all_sessions: Boolean = false, base_sessions: List[String] = Nil, @@ -636,7 +672,7 @@ val numa_node = numa_nodes.next(used_node) val job = - new Job(progress, name, info, deps, store, do_store, verbose, pide = pide, + new Job(progress, name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(name)) loop(pending, running + (name -> (ancestor_heaps, job)), results) } @@ -724,7 +760,6 @@ var base_sessions: List[String] = Nil var select_dirs: List[Path] = Nil var numa_shuffling = false - var pide = false var requirements = false var soft_build = false var exclude_session_groups: List[String] = Nil @@ -750,7 +785,6 @@ -B NAME include session NAME and all descendants -D DIR include session directory and select its sessions -N cyclic shuffling of NUMA CPU nodes (performance tuning) - -P build via PIDE protocol -R operate on requirements of selected sessions -S soft build: only observe changes of sources, not heap images -X NAME exclude sessions from group NAME and all descendants @@ -775,7 +809,6 @@ "B:" -> (arg => base_sessions = base_sessions ::: List(arg)), "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))), "N" -> (_ => numa_shuffling = true), - "P" -> (_ => pide = true), "R" -> (_ => requirements = true), "S" -> (_ => soft_build = true), "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)), @@ -825,7 +858,6 @@ soft_build = soft_build, verbose = verbose, export_files = export_files, - pide = pide, requirements = requirements, all_sessions = all_sessions, base_sessions = base_sessions, diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Pure/Tools/simplifier_trace.scala Wed Apr 01 23:04:28 2020 +0200 @@ -123,22 +123,22 @@ def handle_results(session: Session, id: Document_ID.Command, results: Command.Results): Context = { val slot = Future.promise[Context] - manager.send(Handle_Results(session, id, results, slot)) + the_manager(session).send(Handle_Results(session, id, results, slot)) slot.join } - def generate_trace(results: Command.Results): Trace = + def generate_trace(session: Session, results: Command.Results): Trace = { val slot = Future.promise[Trace] - manager.send(Generate_Trace(results, slot)) + the_manager(session).send(Generate_Trace(results, slot)) slot.join } - def clear_memory() = - manager.send(Clear_Memory) + def clear_memory(session: Session): Unit = + the_manager(session).send(Clear_Memory) - def send_reply(session: Session, serial: Long, answer: Answer) = - manager.send(Reply(session, serial, answer)) + def send_reply(session: Session, serial: Long, answer: Answer): Unit = + the_manager(session).send(Reply(session, serial, answer)) def make_manager: Consumer_Thread[Any] = { @@ -283,10 +283,10 @@ ) } - private val manager_variable = Synchronized[Option[Consumer_Thread[Any]]](None) + private val managers = Synchronized(Map.empty[Session, Consumer_Thread[Any]]) - def manager: Consumer_Thread[Any] = - manager_variable.value match { + def the_manager(session: Session): Consumer_Thread[Any] = + managers.value.get(session) match { case Some(thread) if thread.is_active => thread case _ => error("Bad Simplifier_Trace.manager thread") } @@ -296,20 +296,31 @@ class Handler extends Session.Protocol_Handler { - try { manager } - catch { case ERROR(_) => manager_variable.change(_ => Some(make_manager)) } + private var the_session: Session = null + + override def init(session: Session) + { + try { the_manager(session) } + catch { case ERROR(_) => managers.change(map => map + (session -> make_manager)) } + the_session = session + } - override def exit() = + override def exit() { - manager.send(Clear_Memory) - manager.shutdown() - manager_variable.change(_ => None) + val session = the_session + if (session != null) { + val manager = the_manager(session) + manager.send(Clear_Memory) + manager.shutdown() + managers.change(map => map - session) + the_session = null + } } private def cancel(msg: Prover.Protocol_Output): Boolean = msg.properties match { case Markup.Simp_Trace_Cancel(serial) => - manager.send(Cancel(serial)) + the_manager(the_session).send(Cancel(serial)) true case _ => false diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Tools/VSCode/src/vscode_resources.scala --- a/src/Tools/VSCode/src/vscode_resources.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Tools/VSCode/src/vscode_resources.scala Wed Apr 01 23:04:28 2020 +0200 @@ -345,7 +345,7 @@ output_text(XML.content(xml)) def output_pretty(body: XML.Body, margin: Int): String = - output_text(Pretty.string_of(body, margin = margin)) + output_text(Pretty.string_of(body, margin = margin, metric = Symbol.Metric)) def output_pretty_tooltip(body: XML.Body): String = output_pretty(body, tooltip_margin) def output_pretty_message(body: XML.Body): String = output_pretty(body, message_margin) diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Tools/jEdit/src/monitor_dockable.scala --- a/src/Tools/jEdit/src/monitor_dockable.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Tools/jEdit/src/monitor_dockable.scala Wed Apr 01 23:04:28 2020 +0200 @@ -108,7 +108,7 @@ private val main = Session.Consumer[Any](getClass.getName) { - case stats: Session.Statistics => + case stats: Session.Runtime_Statistics => add_statistics(stats.props) update_delay.invoke() @@ -118,13 +118,13 @@ override def init() { - PIDE.session.statistics += main + PIDE.session.runtime_statistics += main PIDE.session.global_options += main } override def exit() { - PIDE.session.statistics -= main + PIDE.session.runtime_statistics -= main PIDE.session.global_options -= main } } diff -r 9d8fb1dbc368 -r 0aef1812ae3a src/Tools/jEdit/src/simplifier_trace_dockable.scala --- a/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Apr 01 21:48:39 2020 +0200 +++ b/src/Tools/jEdit/src/simplifier_trace_dockable.scala Wed Apr 01 23:04:28 2020 +0200 @@ -64,7 +64,7 @@ private def show_trace() { - val trace = Simplifier_Trace.generate_trace(current_results) + val trace = Simplifier_Trace.generate_trace(PIDE.session, current_results) new Simplifier_Trace_Window(view, current_snapshot, trace) } @@ -181,7 +181,7 @@ new Button("Clear memory") { reactions += { case ButtonClicked(_) => - Simplifier_Trace.clear_memory() + Simplifier_Trace.clear_memory(PIDE.session) } }))