shared output primitives of physical/virtual Pure;
authorwenzelm
Sat Apr 09 16:16:05 2016 +0200 (2016-04-09)
changeset 6293051ac6bc389e8
parent 62929 b92565f98206
child 62931 09b516854210
shared output primitives of physical/virtual Pure;
src/Pure/General/output.ML
src/Pure/General/output.scala
src/Pure/General/output_primitives.ML
src/Pure/General/output_primitives_virtual.ML
src/Pure/ML/ml_name_space.ML
src/Pure/ML_Bootstrap.thy
src/Pure/ROOT.ML
src/Pure/ROOT0.ML
src/Pure/System/isabelle_process.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/General/output.ML	Sat Apr 09 14:52:10 2016 +0200
     1.2 +++ b/src/Pure/General/output.ML	Sat Apr 09 16:16:05 2016 +0200
     1.3 @@ -1,7 +1,7 @@
     1.4  (*  Title:      Pure/General/output.ML
     1.5 -    Author:     Makarius, Hagia Maria Sion Abbey (Jerusalem)
     1.6 +    Author:     Makarius
     1.7  
     1.8 -Isabelle channels for diagnostic output.
     1.9 +Isabelle output channels.
    1.10  *)
    1.11  
    1.12  signature BASIC_OUTPUT =
    1.13 @@ -59,7 +59,7 @@
    1.14    val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref
    1.15  end;
    1.16  
    1.17 -structure Output: PRIVATE_OUTPUT =
    1.18 +structure Private_Output: PRIVATE_OUTPUT =
    1.19  struct
    1.20  
    1.21  (** print modes **)
    1.22 @@ -90,7 +90,23 @@
    1.23  
    1.24  (** output channels **)
    1.25  
    1.26 -(* raw output primitives -- not to be used in user-space *)
    1.27 +(* primitives -- provided via bootstrap environment *)
    1.28 +
    1.29 +val writeln_fn = Unsynchronized.ref Output_Primitives.writeln_fn;
    1.30 +val state_fn = Unsynchronized.ref Output_Primitives.state_fn;
    1.31 +val information_fn = Unsynchronized.ref Output_Primitives.information_fn;
    1.32 +val tracing_fn = Unsynchronized.ref Output_Primitives.tracing_fn;
    1.33 +val warning_fn = Unsynchronized.ref Output_Primitives.warning_fn;
    1.34 +val legacy_fn = Unsynchronized.ref Output_Primitives.legacy_fn;
    1.35 +val error_message_fn = Unsynchronized.ref Output_Primitives.error_message_fn;
    1.36 +val system_message_fn = Unsynchronized.ref Output_Primitives.system_message_fn;
    1.37 +val status_fn = Unsynchronized.ref Output_Primitives.status_fn;
    1.38 +val report_fn = Unsynchronized.ref Output_Primitives.report_fn;
    1.39 +val result_fn = Unsynchronized.ref Output_Primitives.result_fn;
    1.40 +val protocol_message_fn = Unsynchronized.ref Output_Primitives.protocol_message_fn;
    1.41 +
    1.42 +
    1.43 +(* physical output -- not to be used in user-space *)
    1.44  
    1.45  fun physical_stdout s = (TextIO.output (TextIO.stdOut, s); TextIO.flushOut TextIO.stdOut);
    1.46  fun physical_stderr s = (TextIO.output (TextIO.stdErr, s); TextIO.flushOut TextIO.stdErr);
    1.47 @@ -103,21 +119,18 @@
    1.48  
    1.49  exception Protocol_Message of Properties.T;
    1.50  
    1.51 -val writeln_fn = Unsynchronized.ref (physical_writeln o implode);
    1.52 -val state_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.53 -val information_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.54 -val tracing_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.55 -val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### " o implode);
    1.56 -val legacy_fn = Unsynchronized.ref (fn ss => ! warning_fn ss);
    1.57 -
    1.58 -val error_message_fn =
    1.59 -  Unsynchronized.ref (fn (_: serial, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.60 -val system_message_fn = Unsynchronized.ref (fn ss => ! writeln_fn ss);
    1.61 -val status_fn = Unsynchronized.ref (fn _: output list => ());
    1.62 -val report_fn = Unsynchronized.ref (fn _: output list => ());
    1.63 -val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output list => ());
    1.64 -val protocol_message_fn: (Properties.T -> output list -> unit) Unsynchronized.ref =
    1.65 -  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.66 +val _ =
    1.67 +  if Thread_Data.is_virtual then ()
    1.68 +  else
    1.69 +   (writeln_fn := (physical_writeln o implode);
    1.70 +    state_fn := (fn ss => ! writeln_fn ss);
    1.71 +    information_fn := (fn ss => ! writeln_fn ss);
    1.72 +    tracing_fn := (fn ss => ! writeln_fn ss);
    1.73 +    warning_fn := (physical_writeln o prefix_lines "### " o implode);
    1.74 +    legacy_fn := (fn ss => ! warning_fn ss);
    1.75 +    error_message_fn := (fn (_, ss) => physical_writeln (prefix_lines "*** " (implode ss)));
    1.76 +    system_message_fn := (fn ss => ! writeln_fn ss);
    1.77 +    protocol_message_fn := (fn props => fn _ => raise Protocol_Message props));
    1.78  
    1.79  fun writelns ss = ! writeln_fn (map output ss);
    1.80  fun writeln s = writelns [s];
    1.81 @@ -171,5 +184,6 @@
    1.82  
    1.83  end;
    1.84  
    1.85 +structure Output: OUTPUT = Private_Output;
    1.86  structure Basic_Output: BASIC_OUTPUT = Output;
    1.87  open Basic_Output;
     2.1 --- a/src/Pure/General/output.scala	Sat Apr 09 14:52:10 2016 +0200
     2.2 +++ b/src/Pure/General/output.scala	Sat Apr 09 16:16:05 2016 +0200
     2.3 @@ -2,7 +2,7 @@
     2.4      Module:     PIDE
     2.5      Author:     Makarius
     2.6  
     2.7 -Isabelle channels for diagnostic output.
     2.8 +Isabelle output channels.
     2.9  */
    2.10  
    2.11  package isabelle
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/General/output_primitives.ML	Sat Apr 09 16:16:05 2016 +0200
     3.3 @@ -0,0 +1,48 @@
     3.4 +(*  Title:      Pure/General/output_primitives.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Primitives for Isabelle output channels.
     3.8 +*)
     3.9 +
    3.10 +signature OUTPUT_PRIMITIVES =
    3.11 +sig
    3.12 +  type output = string
    3.13 +  type serial = int
    3.14 +  type properties = (string * string) list
    3.15 +  val writeln_fn: output list -> unit
    3.16 +  val state_fn: output list -> unit
    3.17 +  val information_fn: output list -> unit
    3.18 +  val tracing_fn: output list -> unit
    3.19 +  val warning_fn: output list -> unit
    3.20 +  val legacy_fn: output list -> unit
    3.21 +  val error_message_fn: serial * output list -> unit
    3.22 +  val system_message_fn: output list -> unit
    3.23 +  val status_fn: output list -> unit
    3.24 +  val report_fn: output list -> unit
    3.25 +  val result_fn: properties -> output list -> unit
    3.26 +  val protocol_message_fn: properties -> output list -> unit
    3.27 +end;
    3.28 +
    3.29 +structure Output_Primitives: OUTPUT_PRIMITIVES =
    3.30 +struct
    3.31 +
    3.32 +type output = string;
    3.33 +type serial = int;
    3.34 +type properties = (string * string) list;
    3.35 +
    3.36 +fun ignore_outputs (_: output list) = ();
    3.37 +
    3.38 +val writeln_fn = ignore_outputs;
    3.39 +val state_fn = ignore_outputs;
    3.40 +val information_fn = ignore_outputs;
    3.41 +val tracing_fn = ignore_outputs;
    3.42 +val warning_fn = ignore_outputs;
    3.43 +val legacy_fn = ignore_outputs;
    3.44 +fun error_message_fn (_: serial, _: output list) = ();
    3.45 +val system_message_fn = ignore_outputs;
    3.46 +val status_fn = ignore_outputs;
    3.47 +val report_fn = ignore_outputs;
    3.48 +fun result_fn (_: properties) = ignore_outputs;
    3.49 +fun protocol_message_fn (_: properties) = ignore_outputs;
    3.50 +
    3.51 +end;
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/General/output_primitives_virtual.ML	Sat Apr 09 16:16:05 2016 +0200
     4.3 @@ -0,0 +1,25 @@
     4.4 +(*  Title:      Pure/General/output_primitives.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Primitives for Isabelle output channels -- virtual version within Pure environment.
     4.8 +*)
     4.9 +
    4.10 +structure Output_Primitives_Virtual: OUTPUT_PRIMITIVES =
    4.11 +struct
    4.12 +
    4.13 +open Output_Primitives;
    4.14 +
    4.15 +fun writeln_fn x = ! Private_Output.writeln_fn x;
    4.16 +fun state_fn x = ! Private_Output.state_fn x;
    4.17 +fun information_fn x = ! Private_Output.information_fn x;
    4.18 +fun tracing_fn x = ! Private_Output.tracing_fn x;
    4.19 +fun warning_fn x = ! Private_Output.warning_fn x;
    4.20 +fun legacy_fn x = ! Private_Output.legacy_fn x;
    4.21 +fun error_message_fn x = ! Private_Output.error_message_fn x;
    4.22 +fun system_message_fn x = ! Private_Output.system_message_fn x;
    4.23 +fun status_fn x = ! Private_Output.status_fn x;
    4.24 +fun report_fn x = ! Private_Output.report_fn x;
    4.25 +fun result_fn x y = ! Private_Output.result_fn x y;
    4.26 +fun protocol_message_fn x y = ! Private_Output.protocol_message_fn x y;
    4.27 +
    4.28 +end;
     5.1 --- a/src/Pure/ML/ml_name_space.ML	Sat Apr 09 14:52:10 2016 +0200
     5.2 +++ b/src/Pure/ML/ml_name_space.ML	Sat Apr 09 16:16:05 2016 +0200
     5.3 @@ -65,10 +65,11 @@
     5.4        "chapter", "section", "subsection", "subsubsection", "paragraph", "subparagraph"];
     5.5    val hidden_structures = ["CInterface", "Foreign", "RunCall", "RuntimeCalls", "Signal"];
     5.6    val bootstrap_structures =
     5.7 -    ["Exn", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive", "PolyML"] @
     5.8 -      hidden_structures;
     5.9 +    ["Exn", "Output_Primitives", "Basic_Exn", "Thread_Data", "Thread_Position", "ML_Recursive",
    5.10 +      "Private_Output", "PolyML"] @ hidden_structures;
    5.11    val bootstrap_signatures =
    5.12 -    ["EXN", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE"];
    5.13 +    ["EXN", "OUTPUT_PRIMITIVES", "BASIC_EXN", "THREAD_DATA", "THREAD_POSITION", "ML_RECURSIVE",
    5.14 +      "PRIVATE_OUTPUT"];
    5.15  
    5.16  
    5.17    (* Standard ML environment *)
     6.1 --- a/src/Pure/ML_Bootstrap.thy	Sat Apr 09 14:52:10 2016 +0200
     6.2 +++ b/src/Pure/ML_Bootstrap.thy	Sat Apr 09 16:16:05 2016 +0200
     6.3 @@ -9,7 +9,12 @@
     6.4  begin
     6.5  
     6.6  setup \<open>Context.theory_map ML_Env.init_bootstrap\<close>
     6.7 -SML_import \<open>structure Thread_Data = Thread_Data_Virtual\<close>
     6.8 +
     6.9 +SML_import \<open>
    6.10 +structure Output_Primitives = Output_Primitives_Virtual;
    6.11 +structure Thread_Data = Thread_Data_Virtual;
    6.12 +\<close>
    6.13 +
    6.14  setup \<open>Config.put_global ML_Env.SML_environment true\<close>
    6.15  
    6.16  end
     7.1 --- a/src/Pure/ROOT.ML	Sat Apr 09 14:52:10 2016 +0200
     7.2 +++ b/src/Pure/ROOT.ML	Sat Apr 09 16:16:05 2016 +0200
     7.3 @@ -301,6 +301,7 @@
     7.4  ML_file "System/isabelle_process.ML";
     7.5  ML_file "System/invoke_scala.ML";
     7.6  ML_file "PIDE/protocol.ML";
     7.7 +ML_file "General/output_primitives_virtual.ML";
     7.8  
     7.9  
    7.10  subsection "Miscellaneous tools and packages for Pure Isabelle";
     8.1 --- a/src/Pure/ROOT0.ML	Sat Apr 09 14:52:10 2016 +0200
     8.2 +++ b/src/Pure/ROOT0.ML	Sat Apr 09 16:16:05 2016 +0200
     8.3 @@ -1,6 +1,7 @@
     8.4  (*** Isabelle/Pure bootstrap: initial setup ***)
     8.5  
     8.6  ML_file "General/exn.ML";
     8.7 +ML_file "General/output_primitives.ML";
     8.8  
     8.9  ML_file "Concurrent/thread_attributes.ML";
    8.10  ML_file "Concurrent/thread_data.ML";
     9.1 --- a/src/Pure/System/isabelle_process.ML	Sat Apr 09 14:52:10 2016 +0200
     9.2 +++ b/src/Pure/System/isabelle_process.ML	Sat Apr 09 16:16:05 2016 +0200
     9.3 @@ -114,21 +114,22 @@
     9.4              | _ => props);
     9.5          in message name props' body end;
     9.6    in
     9.7 -    Output.status_fn := standard_message [] Markup.statusN;
     9.8 -    Output.report_fn := standard_message [] Markup.reportN;
     9.9 -    Output.result_fn :=
    9.10 +    Private_Output.status_fn := standard_message [] Markup.statusN;
    9.11 +    Private_Output.report_fn := standard_message [] Markup.reportN;
    9.12 +    Private_Output.result_fn :=
    9.13        (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
    9.14 -    Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    9.15 -    Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
    9.16 -    Output.information_fn := (fn s => standard_message (serial_props ()) Markup.informationN s);
    9.17 -    Output.tracing_fn :=
    9.18 +    Private_Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    9.19 +    Private_Output.state_fn := (fn s => standard_message (serial_props ()) Markup.stateN s);
    9.20 +    Private_Output.information_fn :=
    9.21 +      (fn s => standard_message (serial_props ()) Markup.informationN s);
    9.22 +    Private_Output.tracing_fn :=
    9.23        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
    9.24 -    Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    9.25 -    Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
    9.26 -    Output.error_message_fn :=
    9.27 +    Private_Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    9.28 +    Private_Output.legacy_fn := (fn s => standard_message (serial_props ()) Markup.legacyN s);
    9.29 +    Private_Output.error_message_fn :=
    9.30        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    9.31 -    Output.system_message_fn := message Markup.systemN [];
    9.32 -    Output.protocol_message_fn := message Markup.protocolN;
    9.33 +    Private_Output.system_message_fn := message Markup.systemN [];
    9.34 +    Private_Output.protocol_message_fn := message Markup.protocolN;
    9.35      message Markup.initN [] [Session.welcome ()];
    9.36      msg_channel
    9.37    end;
    10.1 --- a/src/Pure/Tools/build.ML	Sat Apr 09 14:52:10 2016 +0200
    10.2 +++ b/src/Pure/Tools/build.ML	Sat Apr 09 16:16:05 2016 +0200
    10.3 @@ -159,7 +159,7 @@
    10.4        theories |>
    10.5          (List.app (build_theories symbols last_timing Path.current)
    10.6            |> session_timing name verbose
    10.7 -          |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
    10.8 +          |> Unsynchronized.setmp Private_Output.protocol_message_fn protocol_message
    10.9            |> Exn.capture);
   10.10      val res2 = Exn.capture Session.finish ();
   10.11      val _ = Par_Exn.release_all [res1, res2];
   10.12 @@ -193,5 +193,3 @@
   10.13      in Output.protocol_message (Markup.build_theories_result id) [result] end);
   10.14  
   10.15  end;
   10.16 -
   10.17 -structure Output: OUTPUT = Output;  (*seal system channels!*)