# HG changeset patch
# User wenzelm
# Date 1392068344 -3600
# Node ID 51f0876f61dfcdceb04b5af1cb9e00fa89e4a46a
# Parent  0c15ac6edcf768ff2f6b4d5ca5f2946db486d9ef
seal system channels at end of Pure bootstrap -- Isabelle/Scala provides official interfaces;

diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/General/output.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -25,19 +25,6 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
-  structure Internal:
-  sig
-    val writeln_fn: (output -> unit) Unsynchronized.ref
-    val urgent_message_fn: (output -> unit) Unsynchronized.ref
-    val tracing_fn: (output -> unit) Unsynchronized.ref
-    val warning_fn: (output -> unit) Unsynchronized.ref
-    val error_message_fn: (serial * output -> unit) Unsynchronized.ref
-    val prompt_fn: (output -> unit) Unsynchronized.ref
-    val status_fn: (output -> unit) Unsynchronized.ref
-    val report_fn: (output -> unit) Unsynchronized.ref
-    val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
-    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
-  end
   val urgent_message: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
@@ -49,7 +36,22 @@
   val try_protocol_message: Properties.T -> string -> unit
 end;
 
-structure Output: OUTPUT =
+signature PRIVATE_OUTPUT =
+sig
+  include OUTPUT
+  val writeln_fn: (output -> unit) Unsynchronized.ref
+  val urgent_message_fn: (output -> unit) Unsynchronized.ref
+  val tracing_fn: (output -> unit) Unsynchronized.ref
+  val warning_fn: (output -> unit) Unsynchronized.ref
+  val error_message_fn: (serial * output -> unit) Unsynchronized.ref
+  val prompt_fn: (output -> unit) Unsynchronized.ref
+  val status_fn: (output -> unit) Unsynchronized.ref
+  val report_fn: (output -> unit) Unsynchronized.ref
+  val result_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref
+end;
+
+structure Output: PRIVATE_OUTPUT =
 struct
 
 (** print modes **)
@@ -92,33 +94,30 @@
 
 exception Protocol_Message of Properties.T;
 
-structure Internal =
-struct
-  val writeln_fn = Unsynchronized.ref physical_writeln;
-  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
-  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-  val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
-  val error_message_fn =
-    Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
-  val prompt_fn = Unsynchronized.ref physical_stdout;
-  val status_fn = Unsynchronized.ref (fn _: output => ());
-  val report_fn = Unsynchronized.ref (fn _: output => ());
-  val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
-  val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
-end;
+val writeln_fn = Unsynchronized.ref physical_writeln;
+val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);  (*Proof General legacy*)
+val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+val warning_fn = Unsynchronized.ref (physical_writeln o prefix_lines "### ");
+val error_message_fn =
+  Unsynchronized.ref (fn (_: serial, s) => physical_writeln (prefix_lines "*** " s));
+val prompt_fn = Unsynchronized.ref physical_stdout;
+val status_fn = Unsynchronized.ref (fn _: output => ());
+val report_fn = Unsynchronized.ref (fn _: output => ());
+val result_fn = Unsynchronized.ref (fn _: Properties.T => fn _: output => ());
+val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
+  Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 
-fun writeln s = ! Internal.writeln_fn (output s);
-fun urgent_message s = ! Internal.urgent_message_fn (output s);  (*Proof General legacy*)
-fun tracing s = ! Internal.tracing_fn (output s);
-fun warning s = ! Internal.warning_fn (output s);
-fun error_message' (i, s) = ! Internal.error_message_fn (i, output s);
+fun writeln s = ! writeln_fn (output s);
+fun urgent_message s = ! urgent_message_fn (output s);  (*Proof General legacy*)
+fun tracing s = ! tracing_fn (output s);
+fun warning s = ! warning_fn (output s);
+fun error_message' (i, s) = ! error_message_fn (i, output s);
 fun error_message s = error_message' (serial (), s);
-fun prompt s = ! Internal.prompt_fn (output s);
-fun status s = ! Internal.status_fn (output s);
-fun report s = ! Internal.report_fn (output s);
-fun result props s = ! Internal.result_fn props (output s);
-fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
+fun prompt s = ! prompt_fn (output s);
+fun status s = ! status_fn (output s);
+fun report s = ! report_fn (output s);
+fun result props s = ! result_fn props (output s);
+fun protocol_message props s = ! protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 
 end;
diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/ROOT.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -306,6 +306,8 @@
 use "Tools/named_thms.ML";
 use "Tools/proof_general.ML";
 
+structure Output: OUTPUT = Output;  (*seal system channels!*)
+
 
 (* ML toplevel pretty printing *)
 
diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/System/isabelle_process.ML
--- a/src/Pure/System/isabelle_process.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/System/isabelle_process.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -111,19 +111,19 @@
         message name
           (fold_rev Properties.put props (Position.properties_of (Position.thread_data ()))) body;
   in
-    Output.Internal.status_fn := standard_message [] Markup.statusN;
-    Output.Internal.report_fn := standard_message [] Markup.reportN;
-    Output.Internal.result_fn :=
+    Output.status_fn := standard_message [] Markup.statusN;
+    Output.report_fn := standard_message [] Markup.reportN;
+    Output.result_fn :=
       (fn props => fn s => standard_message (props @ serial_props ()) Markup.resultN s);
-    Output.Internal.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
-    Output.Internal.tracing_fn :=
+    Output.writeln_fn := (fn s => standard_message (serial_props ()) Markup.writelnN s);
+    Output.tracing_fn :=
       (fn s => (update_tracing (); standard_message (serial_props ()) Markup.tracingN s));
-    Output.Internal.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
-    Output.Internal.error_message_fn :=
+    Output.warning_fn := (fn s => standard_message (serial_props ()) Markup.warningN s);
+    Output.error_message_fn :=
       (fn (i, s) => standard_message (Markup.serial_properties i) Markup.errorN s);
-    Output.Internal.protocol_message_fn := message Markup.protocolN;
-    Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
-    Output.Internal.prompt_fn := ignore;
+    Output.protocol_message_fn := message Markup.protocolN;
+    Output.urgent_message_fn := ! Output.writeln_fn;
+    Output.prompt_fn := ignore;
     message Markup.initN [] (Session.welcome ());
     msg_channel
   end;
diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/System/isar.ML
--- a/src/Pure/System/isar.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/System/isar.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -157,7 +157,7 @@
  (Context.set_thread_data NONE;
   Multithreading.max_threads_update (Options.default_int "threads");
   if do_init then init () else ();
-  Output.Internal.protocol_message_fn := protocol_message;
+  Output.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 
diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/Tools/build.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -166,7 +166,7 @@
         theories |>
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
-            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
+            |> Unsynchronized.setmp Output.protocol_message_fn protocol_message
             |> Multithreading.max_threads_setmp (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();
diff -r 0c15ac6edcf7 -r 51f0876f61df src/Pure/Tools/proof_general.ML
--- a/src/Pure/Tools/proof_general.ML	Mon Feb 10 22:22:06 2014 +0100
+++ b/src/Pure/Tools/proof_general.ML	Mon Feb 10 22:39:04 2014 +0100
@@ -264,14 +264,14 @@
   | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (Output.Internal.writeln_fn := message "" "" "";
-  Output.Internal.status_fn := (fn _ => ());
-  Output.Internal.report_fn := (fn _ => ());
-  Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
-  Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.Internal.warning_fn := message (special "K") (special "L") "### ";
-  Output.Internal.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (Output.writeln_fn := message "" "" "";
+  Output.status_fn := (fn _ => ());
+  Output.report_fn := (fn _ => ());
+  Output.urgent_message_fn := message (special "I") (special "J") "";
+  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
+  Output.warning_fn := message (special "K") (special "L") "### ";
+  Output.error_message_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+  Output.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 
 (* notification *)