1.1 --- a/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:06:56 2010 +0200
     1.2 +++ b/src/HOL/Mutabelle/MutabelleExtra.thy	Mon Oct 25 21:23:09 2010 +0200
     1.3 @@ -19,10 +19,11 @@
     1.4       "mutabelle_extra.ML"
     1.5  begin
     1.6  
     1.7 -ML {* val old_tr = !Output.tracing_fn *}
     1.8 -ML {* val old_wr = !Output.writeln_fn *}
     1.9 -ML {* val old_ur = !Output.urgent_message_fn *}
    1.10 -ML {* val old_wa = !Output.warning_fn *}
    1.11 +(* FIXME !?!?! *)
    1.12 +ML {* val old_tr = !Output.Private_Hooks.tracing_fn *}
    1.13 +ML {* val old_wr = !Output.Private_Hooks.writeln_fn *}
    1.14 +ML {* val old_ur = !Output.Private_Hooks.urgent_message_fn *}
    1.15 +ML {* val old_wa = !Output.Private_Hooks.warning_fn *}
    1.16  
    1.17  quickcheck_params [size = 5, iterations = 1000]
    1.18  (*
    1.19 @@ -48,9 +49,10 @@
    1.20  *)
    1.21   *}
    1.22  
    1.23 -ML {* Output.tracing_fn := old_tr *}
    1.24 -ML {* Output.writeln_fn := old_wr *}
    1.25 -ML {* Output.urgent_message_fn := old_ur *}
    1.26 -ML {* Output.warning_fn := old_wa *}
    1.27 +(* FIXME !?!?! *)
    1.28 +ML {* Output.Private_Hooks.tracing_fn := old_tr *}
    1.29 +ML {* Output.Private_Hooks.writeln_fn := old_wr *}
    1.30 +ML {* Output.Private_Hooks.urgent_message_fn := old_ur *}
    1.31 +ML {* Output.Private_Hooks.warning_fn := old_wa *}
    1.32  
    1.33  end

     2.1 --- a/src/Pure/General/output.ML	Mon Oct 25 21:06:56 2010 +0200
     2.2 +++ b/src/Pure/General/output.ML	Mon Oct 25 21:23:09 2010 +0200
     2.3 @@ -30,14 +30,17 @@
     2.4    val raw_stdout: output -> unit
     2.5    val raw_stderr: output -> unit
     2.6    val raw_writeln: output -> unit
     2.7 -  val writeln_fn: (output -> unit) Unsynchronized.ref
     2.8 -  val urgent_message_fn: (output -> unit) Unsynchronized.ref
     2.9 -  val tracing_fn: (output -> unit) Unsynchronized.ref
    2.10 -  val warning_fn: (output -> unit) Unsynchronized.ref
    2.11 -  val error_fn: (output -> unit) Unsynchronized.ref
    2.12 -  val prompt_fn: (output -> unit) Unsynchronized.ref
    2.13 -  val status_fn: (output -> unit) Unsynchronized.ref
    2.14 -  val report_fn: (output -> unit) Unsynchronized.ref
    2.15 +  structure Private_Hooks:
    2.16 +  sig
    2.17 +    val writeln_fn: (output -> unit) Unsynchronized.ref
    2.18 +    val urgent_message_fn: (output -> unit) Unsynchronized.ref
    2.19 +    val tracing_fn: (output -> unit) Unsynchronized.ref
    2.20 +    val warning_fn: (output -> unit) Unsynchronized.ref
    2.21 +    val error_fn: (output -> unit) Unsynchronized.ref
    2.22 +    val prompt_fn: (output -> unit) Unsynchronized.ref
    2.23 +    val status_fn: (output -> unit) Unsynchronized.ref
    2.24 +    val report_fn: (output -> unit) Unsynchronized.ref
    2.25 +  end
    2.26    val urgent_message: string -> unit
    2.27    val error_msg: string -> unit
    2.28    val prompt: string -> unit
    2.29 @@ -85,23 +88,26 @@
    2.30  
    2.31  (* Isabelle output channels *)
    2.32  
    2.33 -val writeln_fn = Unsynchronized.ref raw_writeln;
    2.34 -val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.35 -val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.36 -val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.37 -val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    2.38 -val prompt_fn = Unsynchronized.ref raw_stdout;
    2.39 -val status_fn = Unsynchronized.ref (fn _: string => ());
    2.40 -val report_fn = Unsynchronized.ref (fn _: string => ());
    2.41 +structure Private_Hooks =
    2.42 +struct
    2.43 +  val writeln_fn = Unsynchronized.ref raw_writeln;
    2.44 +  val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.45 +  val tracing_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    2.46 +  val warning_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "### ");
    2.47 +  val error_fn = Unsynchronized.ref (raw_stdout o suffix "\n" o prefix_lines "*** ");
    2.48 +  val prompt_fn = Unsynchronized.ref raw_stdout;
    2.49 +  val status_fn = Unsynchronized.ref (fn _: string => ());
    2.50 +  val report_fn = Unsynchronized.ref (fn _: string => ());
    2.51 +end;
    2.52  
    2.53 -fun writeln s = ! writeln_fn (output s);
    2.54 -fun urgent_message s = ! urgent_message_fn (output s);
    2.55 -fun tracing s = ! tracing_fn (output s);
    2.56 -fun warning s = ! warning_fn (output s);
    2.57 -fun error_msg s = ! error_fn (output s);
    2.58 -fun prompt s = ! prompt_fn (output s);
    2.59 -fun status s = ! status_fn (output s);
    2.60 -fun report s = ! report_fn (output s);
    2.61 +fun writeln s = ! Private_Hooks.writeln_fn (output s);
    2.62 +fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
    2.63 +fun tracing s = ! Private_Hooks.tracing_fn (output s);
    2.64 +fun warning s = ! Private_Hooks.warning_fn (output s);
    2.65 +fun error_msg s = ! Private_Hooks.error_fn (output s);
    2.66 +fun prompt s = ! Private_Hooks.prompt_fn (output s);
    2.67 +fun status s = ! Private_Hooks.status_fn (output s);
    2.68 +fun report s = ! Private_Hooks.report_fn (output s);
    2.69  
    2.70  fun legacy_feature s = warning ("Legacy feature! " ^ s);
    2.71  

     3.1 --- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 21:06:56 2010 +0200
     3.2 +++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Mon Oct 25 21:23:09 2010 +0200
     3.3 @@ -74,14 +74,14 @@
     3.4    | s => Output.raw_writeln (enclose bg en (prefix_lines prfx s)));
     3.5  
     3.6  fun setup_messages () =
     3.7 - (Output.writeln_fn := message "" "" "";
     3.8 -  Output.status_fn := (fn _ => ());
     3.9 -  Output.report_fn := (fn _ => ());
    3.10 -  Output.urgent_message_fn := message (special "I") (special "J") "";
    3.11 -  Output.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    3.12 -  Output.warning_fn := message (special "K") (special "L") "### ";
    3.13 -  Output.error_fn := message (special "M") (special "N") "*** ";
    3.14 -  Output.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
    3.15 + (Output.Private_Hooks.writeln_fn := message "" "" "";
    3.16 +  Output.Private_Hooks.status_fn := (fn _ => ());
    3.17 +  Output.Private_Hooks.report_fn := (fn _ => ());
    3.18 +  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
    3.19 +  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    3.20 +  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
    3.21 +  Output.Private_Hooks.error_fn := message (special "M") (special "N") "*** ";
    3.22 +  Output.Private_Hooks.prompt_fn := (fn s => Output.raw_stdout (render s ^ special "S")));
    3.23  
    3.24  fun panic s =
    3.25    (message (special "M") (special "N") "!!! " ("## SYSTEM EXIT ##\n" ^ s); exit 1);
    3.26 @@ -227,7 +227,7 @@
    3.27            Output.default_output Output.default_escape;
    3.28           Markup.add_mode ProofGeneralPgip.proof_general_emacsN YXML.output_markup;
    3.29           setup_messages ();
    3.30 -         ProofGeneralPgip.pgip_channel_emacs (! Output.urgent_message_fn);
    3.31 +         ProofGeneralPgip.pgip_channel_emacs (! Output.Private_Hooks.urgent_message_fn);
    3.32           setup_thy_loader ();
    3.33           setup_present_hook ();
    3.34           initialized := true);

     4.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 21:06:56 2010 +0200
     4.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Oct 25 21:23:09 2010 +0200
     4.3 @@ -160,13 +160,13 @@
     4.4     add new lines explicitly in PGIP: they are left implicit.  It means that PGIP messages
     4.5     can't be written without newlines. *)
     4.6  fun setup_messages () =
     4.7 - (Output.writeln_fn := (fn s => normalmsg Message s);
     4.8 -  Output.status_fn := (fn _ => ());
     4.9 -  Output.report_fn := (fn _ => ());
    4.10 -  Output.urgent_message_fn := (fn s => normalmsg Status s);
    4.11 -  Output.tracing_fn := (fn s => normalmsg Tracing s);
    4.12 -  Output.warning_fn := (fn s => errormsg Message Warning s);
    4.13 -  Output.error_fn := (fn s => errormsg Message Fatal s));
    4.14 + (Output.Private_Hooks.writeln_fn := (fn s => normalmsg Message s);
    4.15 +  Output.Private_Hooks.status_fn := (fn _ => ());
    4.16 +  Output.Private_Hooks.report_fn := (fn _ => ());
    4.17 +  Output.Private_Hooks.urgent_message_fn := (fn s => normalmsg Status s);
    4.18 +  Output.Private_Hooks.tracing_fn := (fn s => normalmsg Tracing s);
    4.19 +  Output.Private_Hooks.warning_fn := (fn s => errormsg Message Warning s);
    4.20 +  Output.Private_Hooks.error_fn := (fn s => errormsg Message Fatal s));
    4.21  
    4.22  
    4.23  (* immediate messages *)

     5.1 --- a/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:06:56 2010 +0200
     5.2 +++ b/src/Pure/System/isabelle_process.ML	Mon Oct 25 21:23:09 2010 +0200
     5.3 @@ -106,14 +106,14 @@
     5.4      val _ = Simple_Thread.fork false (auto_flush TextIO.stdOut);
     5.5      val _ = Simple_Thread.fork false (auto_flush TextIO.stdErr);
     5.6    in
     5.7 -    Output.status_fn := standard_message out_stream false "B";
     5.8 -    Output.report_fn := standard_message out_stream false "C";
     5.9 -    Output.writeln_fn := standard_message out_stream true "D";
    5.10 -    Output.tracing_fn := standard_message out_stream true "E";
    5.11 -    Output.warning_fn := standard_message out_stream true "F";
    5.12 -    Output.error_fn := standard_message out_stream true "G";
    5.13 -    Output.urgent_message_fn := ! Output.writeln_fn;
    5.14 -    Output.prompt_fn := ignore;
    5.15 +    Output.Private_Hooks.status_fn := standard_message out_stream false "B";
    5.16 +    Output.Private_Hooks.report_fn := standard_message out_stream false "C";
    5.17 +    Output.Private_Hooks.writeln_fn := standard_message out_stream true "D";
    5.18 +    Output.Private_Hooks.tracing_fn := standard_message out_stream true "E";
    5.19 +    Output.Private_Hooks.warning_fn := standard_message out_stream true "F";
    5.20 +    Output.Private_Hooks.error_fn := standard_message out_stream true "G";
    5.21 +    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    5.22 +    Output.Private_Hooks.prompt_fn := ignore;
    5.23      (in_stream, out_stream)
    5.24    end;
    5.25