more explicit indication of Output.Private_Hooks (still public to accomodate clones of Proof General for now);

--- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:23:09 2010 +0200
@@ -19,10 +19,11 @@
      "mutabelle_extra.ML"
 begin
 
-ML {* val old_tr = !Output.tracing_fn *}
-ML {* val old_wr = !Output.writeln_fn *}
-ML {* val old_ur = !Output.urgent_message_fn *}
-ML {* val old_wa = !Output.warning_fn *}
+(* FIXME !?!?! *)
+ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
+ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
+ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
+ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
 
 quickcheck_params [size = 5, iterations = 1000]
 (*
@@ -48,9 +49,10 @@
 *)
  *}
 
-ML {* Output.tracing_fn := old_tr *}
-ML {* Output.writeln_fn := old_wr *}
-ML {* Output.urgent_message_fn := old_ur *}
-ML {* Output.warning_fn := old_wa *}
+(* FIXME !?!?! *)
+ML {* Output.Private_Hooks.tracing_fn := old_tr *}
+ML {* Output.Private_Hooks.writeln_fn := old_wr *}
+ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
+ML {* Output.Private_Hooks.warning_fn := old_wa *}
 
 end

--- a/src/Pure/General/output.ML	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/Pure/General/output.ML	Mon Oct 25 21:23:09 2010 +0200
@@ -30,14 +30,17 @@
   val raw_stdout: output -> unit
   val raw_stderr: output -> unit
   val raw_writeln: output -> unit
-  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_fn: (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
+  structure Private_Hooks:
+  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_fn: (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
+  end
   val urgent_message: string -> unit
   val error_msg: string -> unit
   val prompt: string -> unit
@@ -85,23 +88,26 @@
 
 (* Isabelle output channels *)
 
-val writeln_fn = Unsynchronized.ref raw_writeln;
-val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
-val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
-val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
-val prompt_fn = Unsynchronized.ref raw_stdout;
-val status_fn = Unsynchronized.ref (fn _: string => ());
-val report_fn = Unsynchronized.ref (fn _: string => ());
+structure Private_Hooks =
+struct
+  val writeln_fn = Unsynchronized.ref raw_writeln;
+  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
+  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
+  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
+  val prompt_fn = Unsynchronized.ref raw_stdout;
+  val status_fn = Unsynchronized.ref (fn _: string => ());
+  val report_fn = Unsynchronized.ref (fn _: string => ());
+end;
 
-fun writeln s = ! writeln_fn (output s);
-fun urgent_message s = ! urgent_message_fn (output s);
-fun tracing s = ! tracing_fn (output s);
-fun warning s = ! warning_fn (output s);
-fun error_msg s = ! error_fn (output s);
-fun prompt s = ! prompt_fn (output s);
-fun status s = ! status_fn (output s);
-fun report s = ! report_fn (output s);
+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 s = ! Private_Hooks.error_fn (output 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 legacy_feature s = warning ("Legacy feature! " ^ s);
 

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 21:23:09 2010 +0200
@@ -74,14 +74,14 @@
   | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
 
 fun setup_messages () =
- (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_fn := message (special "M") (special "N") "*** ";
-  Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
+ (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 := message (special "M") (special "N") "*** ";
+  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
 
 fun panic s =
   (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
@@ -227,7 +227,7 @@
           Output.default_output Output.default_escape;
          Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
          setup_messages ();
-         ProofGeneralPgip.pgip_channel_emacs (! Output.urgent_message_fn);
+         ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
          setup_thy_loader ();
          setup_present_hook ();
          initialized := true);

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 21:23:09 2010 +0200
@@ -160,13 +160,13 @@
    add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
    can't be written without newlines. *)
 fun setup_messages () =
- (Output.writeln_fn := (fn s => normalmsg Message s);
-  Output.status_fn := (fn _ => ());
-  Output.report_fn := (fn _ => ());
-  Output.urgent_message_fn := (fn s => normalmsg Status s);
-  Output.tracing_fn := (fn s => normalmsg Tracing s);
-  Output.warning_fn := (fn s => errormsg Message Warning s);
-  Output.error_fn := (fn s => errormsg Message Fatal s));
+ (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s);
+  Output.Private_Hooks.status_fn := (fn _ => ());
+  Output.Private_Hooks.report_fn := (fn _ => ());
+  Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
+  Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
+  Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
+  Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
 
 
 (* immediate messages *)

--- a/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:06:56 2010 +0200
+++ b/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:23:09 2010 +0200
@@ -106,14 +106,14 @@
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
   in
-    Output.status_fn := standard_message out_stream false "B";
-    Output.report_fn := standard_message out_stream false "C";
-    Output.writeln_fn := standard_message out_stream true "D";
-    Output.tracing_fn := standard_message out_stream true "E";
-    Output.warning_fn := standard_message out_stream true "F";
-    Output.error_fn := standard_message out_stream true "G";
-    Output.urgent_message_fn := ! Output.writeln_fn;
-    Output.prompt_fn := ignore;
+    Output.Private_Hooks.status_fn := standard_message out_stream false "B";
+    Output.Private_Hooks.report_fn := standard_message out_stream false "C";
+    Output.Private_Hooks.writeln_fn := standard_message out_stream true "D";
+    Output.Private_Hooks.tracing_fn := standard_message out_stream true "E";
+    Output.Private_Hooks.warning_fn := standard_message out_stream true "F";
+    Output.Private_Hooks.error_fn := standard_message out_stream true "G";
+    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
+    Output.Private_Hooks.prompt_fn := ignore;
     (in_stream, out_stream)
   end;