--- 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"
--- 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 =
{
--- 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 =
--- 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)
{
--- 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<long" s then 2
- else if String.isPrefix "\092<Long" s then 2
- else 1;
+ if String.isPrefix "\092<long" s orelse String.isPrefix "\092<Long" s then 2
+ else if is_printable s then 1
+ else 0;
fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
--- 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("\\<long") || sym.startsWith("\\<Long")) 2
+ else if (is_printable(sym)) 1
+ else 0
+ }).sum
+ }
}
--- a/src/Pure/ML/ml_process.scala Wed Apr 01 21:48:39 2020 +0200
+++ b/src/Pure/ML/ml_process.scala Wed Apr 01 23:04:28 2020 +0200
@@ -16,9 +16,11 @@
sessions_structure: Sessions.Structure,
store: Sessions.Store,
logic: String = "",
+ raw_ml_system: Boolean = false,
+ use_prelude: List[String] = Nil,
+ eval_main: String = "",
args: List[String] = Nil,
modes: List[String] = Nil,
- raw_ml_system: Boolean = false,
cwd: JFile = null,
env: Map[String, String] = Isabelle_System.settings(),
redirect: Boolean = false,
@@ -100,9 +102,11 @@
// process
val eval_process =
- if (heaps.isEmpty)
- List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
- else List("Isabelle_Process.init ()")
+ proper_string(eval_main).getOrElse(
+ if (heaps.isEmpty) {
+ "PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth"))
+ }
+ else "Isabelle_Process.init ()")
// ISABELLE_TMP
val isabelle_tmp = Isabelle_System.tmp_dir("process")
@@ -123,8 +127,8 @@
// bash
val bash_args =
ml_runtime_options :::
- (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process)
- .flatMap(eval => 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 """ +
--- 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
}
--- 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)
--- 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()
}
--- 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>\<open>system_channel_address\<close>;
val password = Options.default_string \<^system_option>\<open>system_channel_password\<close>;
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;
--- 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
--- 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)
--- 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 =
{
--- 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,
--- 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
--- 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)
--- 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
}
}
--- 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)
}
}))