tuned signature;

--- a/src/Pure/General/output.ML	Fri Aug 02 16:02:06 2013 +0200
+++ b/src/Pure/General/output.ML	Fri Aug 02 20:47:02 2013 +0200
@@ -25,7 +25,7 @@
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
   exception Protocol_Message of Properties.T
-  structure Private_Hooks:
+  structure Internal:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
     val urgent_message_fn: (output -> unit) Unsynchronized.ref
@@ -92,7 +92,7 @@
 
 exception Protocol_Message of Properties.T;
 
-structure Private_Hooks =
+structure Internal =
 struct
   val writeln_fn = Unsynchronized.ref physical_writeln;
   val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
@@ -107,17 +107,17 @@
     Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 end;
 
-fun writeln s = ! Private_Hooks.writeln_fn (output s);
-fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
-fun tracing s = ! Private_Hooks.tracing_fn (output s);
-fun warning s = ! Private_Hooks.warning_fn (output s);
-fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
+fun writeln s = ! Internal.writeln_fn (output s);
+fun urgent_message s = ! Internal.urgent_message_fn (output s);
+fun tracing s = ! Internal.tracing_fn (output s);
+fun warning s = ! Internal.warning_fn (output s);
+fun error_msg' (i, s) = ! Internal.error_fn (i, output s);
 fun error_msg s = error_msg' (serial (), s);
-fun prompt s = ! Private_Hooks.prompt_fn (output s);
-fun status s = ! Private_Hooks.status_fn (output s);
-fun report s = ! Private_Hooks.report_fn (output s);
-fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
-fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output 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 (i, s) = ! Internal.result_fn (i, output s);
+fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
 fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 
 end;

--- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 16:02:06 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 20:47:02 2013 +0200
@@ -110,20 +110,17 @@
           ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
             (Position.properties_of (Position.thread_data ()))) body;
   in
-    Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
-    Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
-    Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
-    Output.Private_Hooks.writeln_fn :=
-      (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
-    Output.Private_Hooks.tracing_fn :=
+    Output.Internal.status_fn := standard_message NONE Markup.statusN;
+    Output.Internal.report_fn := standard_message NONE Markup.reportN;
+    Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
+    Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
+    Output.Internal.tracing_fn :=
       (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
-    Output.Private_Hooks.warning_fn :=
-      (fn s => standard_message (SOME (serial ())) Markup.warningN s);
-    Output.Private_Hooks.error_fn :=
-      (fn (i, s) => standard_message (SOME i) Markup.errorN s);
-    Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
-    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
-    Output.Private_Hooks.prompt_fn := ignore;
+    Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
+    Output.Internal.error_fn := (fn (i, s) => standard_message (SOME 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;
     message Markup.initN [] (Session.welcome ());
     msg_channel
   end;

--- a/src/Pure/System/isar.ML	Fri Aug 02 16:02:06 2013 +0200
+++ b/src/Pure/System/isar.ML	Fri Aug 02 20:47:02 2013 +0200
@@ -156,7 +156,7 @@
 fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
  (Context.set_thread_data NONE;
   if do_init then init () else ();
-  Output.Private_Hooks.protocol_message_fn := protocol_message;
+  Output.Internal.protocol_message_fn := protocol_message;
   if welcome then writeln (Session.welcome ()) else ();
   uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
 

--- a/src/Pure/Tools/build.ML	Fri Aug 02 16:02:06 2013 +0200
+++ b/src/Pure/Tools/build.ML	Fri Aug 02 20:47:02 2013 +0200
@@ -164,7 +164,7 @@
         theories |>
           (List.app (use_theories_condition last_timing)
             |> session_timing name verbose
-            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
+            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
             |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
             |> Exn.capture);
       val res2 = Exn.capture Session.finish ();

--- a/src/Pure/Tools/proof_general.ML	Fri Aug 02 16:02:06 2013 +0200
+++ b/src/Pure/Tools/proof_general.ML	Fri Aug 02 20:47:02 2013 +0200
@@ -261,14 +261,14 @@
   | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (Output.Private_Hooks.writeln_fn := message "" "" "";
-  Output.Private_Hooks.status_fn := (fn _ => ());
-  Output.Private_Hooks.report_fn := (fn _ => ());
-  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
-  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
-  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
-  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
-  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
+ (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_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
+  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
 
 
 (* notification *)