--- a/src/Pure/General/output.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/General/output.ML Sat Apr 09 16:16:05 2016 +0200
@@ -1,7 +1,7 @@
(* Title: Pure/General/output.ML
- Author: Makarius, Hagia Maria Sion Abbey (Jerusalem)
+ Author: Makarius
-Isabelle channels for diagnostic output.
+Isabelle output channels.
*)
signature BASIC_OUTPUT =
@@ -59,7 +59,7 @@
val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
end;
-structure Output: PRIVATE_OUTPUT =
+structure Private_Output: PRIVATE_OUTPUT =
struct
(** print modes **)
@@ -90,7 +90,23 @@
(** output channels **)
-(* raw output primitives -- not to be used in user-space *)
+(* primitives -- provided via bootstrap environment *)
+
+val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
+val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
+val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
+val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
+val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
+val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
+val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
+val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
+val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
+val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
+val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
+val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
+
+
+(* physical output -- not to be used in user-space *)
fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
@@ -103,21 +119,18 @@
exception Protocol_Message of Properties.T;
-val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
-val state_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
-val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
-val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
-val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
-val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss);
-
-val error_message_fn =
- Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
-val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
-val status_fn = Unsynchronized.ref (fn _: output list => ());
-val report_fn = Unsynchronized.ref (fn _: output list => ());
-val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
-val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
- Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
+val _ =
+ if Thread_Data.is_virtual then ()
+ else
+ (writeln_fn := (physical_writeln o implode);
+ state_fn := (fn ss => ! writeln_fn ss);
+ information_fn := (fn ss => ! writeln_fn ss);
+ tracing_fn := (fn ss => ! writeln_fn ss);
+ warning_fn := (physical_writeln o prefix_lines "### " o implode);
+ legacy_fn := (fn ss => ! warning_fn ss);
+ error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
+ system_message_fn := (fn ss => ! writeln_fn ss);
+ protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
fun writelns ss = ! writeln_fn (map output ss);
fun writeln s = writelns [s];
@@ -171,5 +184,6 @@
end;
+structure Output: OUTPUT = Private_Output;
structure Basic_Output: BASIC_OUTPUT = Output;
open Basic_Output;
--- a/src/Pure/General/output.scala Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/General/output.scala Sat Apr 09 16:16:05 2016 +0200
@@ -2,7 +2,7 @@
Module: PIDE
Author: Makarius
-Isabelle channels for diagnostic output.
+Isabelle output channels.
*/
package isabelle
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output_primitives.ML Sat Apr 09 16:16:05 2016 +0200
@@ -0,0 +1,48 @@
+(* Title: Pure/General/output_primitives.ML
+ Author: Makarius
+
+Primitives for Isabelle output channels.
+*)
+
+signature OUTPUT_PRIMITIVES =
+sig
+ type output = string
+ type serial = int
+ type properties = (string * string) list
+ val writeln_fn: output list -> unit
+ val state_fn: output list -> unit
+ val information_fn: output list -> unit
+ val tracing_fn: output list -> unit
+ val warning_fn: output list -> unit
+ val legacy_fn: output list -> unit
+ val error_message_fn: serial * output list -> unit
+ val system_message_fn: output list -> unit
+ val status_fn: output list -> unit
+ val report_fn: output list -> unit
+ val result_fn: properties -> output list -> unit
+ val protocol_message_fn: properties -> output list -> unit
+end;
+
+structure Output_Primitives: OUTPUT_PRIMITIVES =
+struct
+
+type output = string;
+type serial = int;
+type properties = (string * string) list;
+
+fun ignore_outputs (_: output list) = ();
+
+val writeln_fn = ignore_outputs;
+val state_fn = ignore_outputs;
+val information_fn = ignore_outputs;
+val tracing_fn = ignore_outputs;
+val warning_fn = ignore_outputs;
+val legacy_fn = ignore_outputs;
+fun error_message_fn (_: serial, _: output list) = ();
+val system_message_fn = ignore_outputs;
+val status_fn = ignore_outputs;
+val report_fn = ignore_outputs;
+fun result_fn (_: properties) = ignore_outputs;
+fun protocol_message_fn (_: properties) = ignore_outputs;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output_primitives_virtual.ML Sat Apr 09 16:16:05 2016 +0200
@@ -0,0 +1,25 @@
+(* Title: Pure/General/output_primitives.ML
+ Author: Makarius
+
+Primitives for Isabelle output channels -- virtual version within Pure environment.
+*)
+
+structure Output_Primitives_Virtual: OUTPUT_PRIMITIVES =
+struct
+
+open Output_Primitives;
+
+fun writeln_fn x = ! Private_Output.writeln_fn x;
+fun state_fn x = ! Private_Output.state_fn x;
+fun information_fn x = ! Private_Output.information_fn x;
+fun tracing_fn x = ! Private_Output.tracing_fn x;
+fun warning_fn x = ! Private_Output.warning_fn x;
+fun legacy_fn x = ! Private_Output.legacy_fn x;
+fun error_message_fn x = ! Private_Output.error_message_fn x;
+fun system_message_fn x = ! Private_Output.system_message_fn x;
+fun status_fn x = ! Private_Output.status_fn x;
+fun report_fn x = ! Private_Output.report_fn x;
+fun result_fn x y = ! Private_Output.result_fn x y;
+fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y;
+
+end;
--- a/src/Pure/ML/ml_name_space.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/ML/ml_name_space.ML Sat Apr 09 16:16:05 2016 +0200
@@ -65,10 +65,11 @@
"chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
val bootstrap_structures =
- ["Exn", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive", "PolyML"] @
- hidden_structures;
+ ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
+ "Private_Output", "PolyML"] @ hidden_structures;
val bootstrap_signatures =
- ["EXN", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE"];
+ ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
+ "PRIVATE_OUTPUT"];
(* Standard ML environment *)
--- a/src/Pure/ML_Bootstrap.thy Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/ML_Bootstrap.thy Sat Apr 09 16:16:05 2016 +0200
@@ -9,7 +9,12 @@
begin
setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
-SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
+
+SML_import \<open>
+structure Output_Primitives = Output_Primitives_Virtual;
+structure Thread_Data = Thread_Data_Virtual;
+\<close>
+
setup \<open>Config.put_global ML_Env.SML_environment true\<close>
end
--- a/src/Pure/ROOT.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/ROOT.ML Sat Apr 09 16:16:05 2016 +0200
@@ -301,6 +301,7 @@
ML_file "System/isabelle_process.ML";
ML_file "System/invoke_scala.ML";
ML_file "PIDE/protocol.ML";
+ML_file "General/output_primitives_virtual.ML";
subsection "Miscellaneous tools and packages for Pure Isabelle";
--- a/src/Pure/ROOT0.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/ROOT0.ML Sat Apr 09 16:16:05 2016 +0200
@@ -1,6 +1,7 @@
(*** Isabelle/Pure bootstrap: initial setup ***)
ML_file "General/exn.ML";
+ML_file "General/output_primitives.ML";
ML_file "Concurrent/thread_attributes.ML";
ML_file "Concurrent/thread_data.ML";
--- a/src/Pure/System/isabelle_process.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/System/isabelle_process.ML Sat Apr 09 16:16:05 2016 +0200
@@ -114,21 +114,22 @@
| _ => props);
in message name props' body end;
in
- Output.status_fn := standard_message [] Markup.statusN;
- Output.report_fn := standard_message [] Markup.reportN;
- Output.result_fn :=
+ 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);
- Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
- Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
- Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s);
- Output.tracing_fn :=
+ 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));
- Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
- Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
- Output.error_message_fn :=
+ 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);
- Output.system_message_fn := message Markup.systemN [];
- Output.protocol_message_fn := message Markup.protocolN;
+ Private_Output.system_message_fn := message Markup.systemN [];
+ Private_Output.protocol_message_fn := message Markup.protocolN;
message Markup.initN [] [Session.welcome ()];
msg_channel
end;
--- a/src/Pure/Tools/build.ML Sat Apr 09 14:52:10 2016 +0200
+++ b/src/Pure/Tools/build.ML Sat Apr 09 16:16:05 2016 +0200
@@ -159,7 +159,7 @@
theories |>
(List.app (build_theories symbols last_timing Path.current)
|> session_timing name verbose
- |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
+ |> Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
|> Exn.capture);
val res2 = Exn.capture Session.finish ();
val _ = Par_Exn.release_all [res1, res2];
@@ -193,5 +193,3 @@
in Output.protocol_message (Markup.build_theories_result id) [result] end);
end;
-
-structure Output: OUTPUT = Output; (*seal system channels!*)