seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
authorwenzelm
Mon Feb 10 22:39:04 2014 +0100 (2014-02-10)
changeset 5538751f0876f61df
parent 55386 0c15ac6edcf7
child 55388 bc34c5774f26
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;
src/Pure/General/output.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isar.ML
src/Pure/Tools/build.ML
src/Pure/Tools/proof_general.ML
     1.1 --- a/src/Pure/General/output.ML	Mon Feb 10 22:22:06 2014 +0100
     1.2 +++ b/src/Pure/General/output.ML	Mon Feb 10 22:39:04 2014 +0100
     1.3 @@ -25,19 +25,6 @@
     1.4    val physical_stderr: output -> unit
     1.5    val physical_writeln: output -> unit
     1.6    exception Protocol_Message of Properties.T
     1.7 -  structure Internal:
     1.8 -  sig
     1.9 -    val writeln_fn: (output -> unit) Unsynchronized.ref
    1.10 -    val urgent_message_fn: (output -> unit) Unsynchronized.ref
    1.11 -    val tracing_fn: (output -> unit) Unsynchronized.ref
    1.12 -    val warning_fn: (output -> unit) Unsynchronized.ref
    1.13 -    val error_message_fn: (serial * output -> unit) Unsynchronized.ref
    1.14 -    val prompt_fn: (output -> unit) Unsynchronized.ref
    1.15 -    val status_fn: (output -> unit) Unsynchronized.ref
    1.16 -    val report_fn: (output -> unit) Unsynchronized.ref
    1.17 -    val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.18 -    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.19 -  end
    1.20    val urgent_message: string -> unit
    1.21    val error_message': serial * string -> unit
    1.22    val error_message: string -> unit
    1.23 @@ -49,7 +36,22 @@
    1.24    val try_protocol_message: Properties.T -> string -> unit
    1.25  end;
    1.26  
    1.27 -structure Output: OUTPUT =
    1.28 +signature PRIVATE_OUTPUT =
    1.29 +sig
    1.30 +  include OUTPUT
    1.31 +  val writeln_fn: (output -> unit) Unsynchronized.ref
    1.32 +  val urgent_message_fn: (output -> unit) Unsynchronized.ref
    1.33 +  val tracing_fn: (output -> unit) Unsynchronized.ref
    1.34 +  val warning_fn: (output -> unit) Unsynchronized.ref
    1.35 +  val error_message_fn: (serial * output -> unit) Unsynchronized.ref
    1.36 +  val prompt_fn: (output -> unit) Unsynchronized.ref
    1.37 +  val status_fn: (output -> unit) Unsynchronized.ref
    1.38 +  val report_fn: (output -> unit) Unsynchronized.ref
    1.39 +  val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.40 +  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
    1.41 +end;
    1.42 +
    1.43 +structure Output: PRIVATE_OUTPUT =
    1.44  struct
    1.45  
    1.46  (** print modes **)
    1.47 @@ -92,33 +94,30 @@
    1.48  
    1.49  exception Protocol_Message of Properties.T;
    1.50  
    1.51 -structure Internal =
    1.52 -struct
    1.53 -  val writeln_fn = Unsynchronized.ref physical_writeln;
    1.54 -  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
    1.55 -  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.56 -  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
    1.57 -  val error_message_fn =
    1.58 -    Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
    1.59 -  val prompt_fn = Unsynchronized.ref physical_stdout;
    1.60 -  val status_fn = Unsynchronized.ref (fn _: output => ());
    1.61 -  val report_fn = Unsynchronized.ref (fn _: output => ());
    1.62 -  val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
    1.63 -  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.64 -    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.65 -end;
    1.66 +val writeln_fn = Unsynchronized.ref physical_writeln;
    1.67 +val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
    1.68 +val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.69 +val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
    1.70 +val error_message_fn =
    1.71 +  Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
    1.72 +val prompt_fn = Unsynchronized.ref physical_stdout;
    1.73 +val status_fn = Unsynchronized.ref (fn _: output => ());
    1.74 +val report_fn = Unsynchronized.ref (fn _: output => ());
    1.75 +val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
    1.76 +val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    1.77 +  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.78  
    1.79 -fun writeln s = ! Internal.writeln_fn (output s);
    1.80 -fun urgent_message s = ! Internal.urgent_message_fn (output s);  (*Proof General legacy*)
    1.81 -fun tracing s = ! Internal.tracing_fn (output s);
    1.82 -fun warning s = ! Internal.warning_fn (output s);
    1.83 -fun error_message' (i, s) = ! Internal.error_message_fn (i, output s);
    1.84 +fun writeln s = ! writeln_fn (output s);
    1.85 +fun urgent_message s = ! urgent_message_fn (output s);  (*Proof General legacy*)
    1.86 +fun tracing s = ! tracing_fn (output s);
    1.87 +fun warning s = ! warning_fn (output s);
    1.88 +fun error_message' (i, s) = ! error_message_fn (i, output s);
    1.89  fun error_message s = error_message' (serial (), s);
    1.90 -fun prompt s = ! Internal.prompt_fn (output s);
    1.91 -fun status s = ! Internal.status_fn (output s);
    1.92 -fun report s = ! Internal.report_fn (output s);
    1.93 -fun result props s = ! Internal.result_fn props (output s);
    1.94 -fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
    1.95 +fun prompt s = ! prompt_fn (output s);
    1.96 +fun status s = ! status_fn (output s);
    1.97 +fun report s = ! report_fn (output s);
    1.98 +fun result props s = ! result_fn props (output s);
    1.99 +fun protocol_message props s = ! protocol_message_fn props (output s);
   1.100  fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
   1.101  
   1.102  end;
     2.1 --- a/src/Pure/ROOT.ML	Mon Feb 10 22:22:06 2014 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Mon Feb 10 22:39:04 2014 +0100
     2.3 @@ -306,6 +306,8 @@
     2.4  use "Tools/named_thms.ML";
     2.5  use "Tools/proof_general.ML";
     2.6  
     2.7 +structure Output: OUTPUT = Output;  (*seal system channels!*)
     2.8 +
     2.9  
    2.10  (* ML toplevel pretty printing *)
    2.11  
     3.1 --- a/src/Pure/System/isabelle_process.ML	Mon Feb 10 22:22:06 2014 +0100
     3.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Feb 10 22:39:04 2014 +0100
     3.3 @@ -111,19 +111,19 @@
     3.4          message name
     3.5            (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
     3.6    in
     3.7 -    Output.Internal.status_fn := standard_message [] Markup.statusN;
     3.8 -    Output.Internal.report_fn := standard_message [] Markup.reportN;
     3.9 -    Output.Internal.result_fn :=
    3.10 +    Output.status_fn := standard_message [] Markup.statusN;
    3.11 +    Output.report_fn := standard_message [] Markup.reportN;
    3.12 +    Output.result_fn :=
    3.13        (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
    3.14 -    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    3.15 -    Output.Internal.tracing_fn :=
    3.16 +    Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
    3.17 +    Output.tracing_fn :=
    3.18        (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
    3.19 -    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    3.20 -    Output.Internal.error_message_fn :=
    3.21 +    Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
    3.22 +    Output.error_message_fn :=
    3.23        (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
    3.24 -    Output.Internal.protocol_message_fn := message Markup.protocolN;
    3.25 -    Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
    3.26 -    Output.Internal.prompt_fn := ignore;
    3.27 +    Output.protocol_message_fn := message Markup.protocolN;
    3.28 +    Output.urgent_message_fn := ! Output.writeln_fn;
    3.29 +    Output.prompt_fn := ignore;
    3.30      message Markup.initN [] (Session.welcome ());
    3.31      msg_channel
    3.32    end;
     4.1 --- a/src/Pure/System/isar.ML	Mon Feb 10 22:22:06 2014 +0100
     4.2 +++ b/src/Pure/System/isar.ML	Mon Feb 10 22:39:04 2014 +0100
     4.3 @@ -157,7 +157,7 @@
     4.4   (Context.set_thread_data NONE;
     4.5    Multithreading.max_threads_update (Options.default_int "threads");
     4.6    if do_init then init () else ();
     4.7 -  Output.Internal.protocol_message_fn := protocol_message;
     4.8 +  Output.protocol_message_fn := protocol_message;
     4.9    if welcome then writeln (Session.welcome ()) else ();
    4.10    uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
    4.11  
     5.1 --- a/src/Pure/Tools/build.ML	Mon Feb 10 22:22:06 2014 +0100
     5.2 +++ b/src/Pure/Tools/build.ML	Mon Feb 10 22:39:04 2014 +0100
     5.3 @@ -166,7 +166,7 @@
     5.4          theories |>
     5.5            (List.app (use_theories_condition last_timing)
     5.6              |> session_timing name verbose
     5.7 -            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
     5.8 +            |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
     5.9              |> Multithreading.max_threads_setmp (Options.int options "threads")
    5.10              |> Exn.capture);
    5.11        val res2 = Exn.capture Session.finish ();
     6.1 --- a/src/Pure/Tools/proof_general.ML	Mon Feb 10 22:22:06 2014 +0100
     6.2 +++ b/src/Pure/Tools/proof_general.ML	Mon Feb 10 22:39:04 2014 +0100
     6.3 @@ -264,14 +264,14 @@
     6.4    | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
     6.5  
     6.6  fun setup_messages () =
     6.7 - (Output.Internal.writeln_fn := message "" "" "";
     6.8 -  Output.Internal.status_fn := (fn _ => ());
     6.9 -  Output.Internal.report_fn := (fn _ => ());
    6.10 -  Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
    6.11 -  Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    6.12 -  Output.Internal.warning_fn := message (special "K") (special "L") "### ";
    6.13 -  Output.Internal.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    6.14 -  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
    6.15 + (Output.writeln_fn := message "" "" "";
    6.16 +  Output.status_fn := (fn _ => ());
    6.17 +  Output.report_fn := (fn _ => ());
    6.18 +  Output.urgent_message_fn := message (special "I") (special "J") "";
    6.19 +  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    6.20 +  Output.warning_fn := message (special "K") (special "L") "### ";
    6.21 +  Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    6.22 +  Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
    6.23  
    6.24  
    6.25  (* notification *)