tuned signature;
authorwenzelm
Fri Aug 02 20:47:02 2013 +0200 (2013-08-02)
changeset 5285208ecbffaf25c
parent 52851 e71b5160f242
child 52853 4ab66773a41f
tuned signature;
src/Pure/General/output.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	Fri Aug 02 16:02:06 2013 +0200
     1.2 +++ b/src/Pure/General/output.ML	Fri Aug 02 20:47:02 2013 +0200
     1.3 @@ -25,7 +25,7 @@
     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 Private_Hooks:
     1.8 +  structure Internal:
     1.9    sig
    1.10      val writeln_fn: (output -> unit) Unsynchronized.ref
    1.11      val urgent_message_fn: (output -> unit) Unsynchronized.ref
    1.12 @@ -92,7 +92,7 @@
    1.13  
    1.14  exception Protocol_Message of Properties.T;
    1.15  
    1.16 -structure Private_Hooks =
    1.17 +structure Internal =
    1.18  struct
    1.19    val writeln_fn = Unsynchronized.ref physical_writeln;
    1.20    val urgent_message_fn = Unsynchronized.ref (fn s => ! writeln_fn s);
    1.21 @@ -107,17 +107,17 @@
    1.22      Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    1.23  end;
    1.24  
    1.25 -fun writeln s = ! Private_Hooks.writeln_fn (output s);
    1.26 -fun urgent_message s = ! Private_Hooks.urgent_message_fn (output s);
    1.27 -fun tracing s = ! Private_Hooks.tracing_fn (output s);
    1.28 -fun warning s = ! Private_Hooks.warning_fn (output s);
    1.29 -fun error_msg' (i, s) = ! Private_Hooks.error_fn (i, output s);
    1.30 +fun writeln s = ! Internal.writeln_fn (output s);
    1.31 +fun urgent_message s = ! Internal.urgent_message_fn (output s);
    1.32 +fun tracing s = ! Internal.tracing_fn (output s);
    1.33 +fun warning s = ! Internal.warning_fn (output s);
    1.34 +fun error_msg' (i, s) = ! Internal.error_fn (i, output s);
    1.35  fun error_msg s = error_msg' (serial (), s);
    1.36 -fun prompt s = ! Private_Hooks.prompt_fn (output s);
    1.37 -fun status s = ! Private_Hooks.status_fn (output s);
    1.38 -fun report s = ! Private_Hooks.report_fn (output s);
    1.39 -fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
    1.40 -fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    1.41 +fun prompt s = ! Internal.prompt_fn (output s);
    1.42 +fun status s = ! Internal.status_fn (output s);
    1.43 +fun report s = ! Internal.report_fn (output s);
    1.44 +fun result (i, s) = ! Internal.result_fn (i, output s);
    1.45 +fun protocol_message props s = ! Internal.protocol_message_fn props (output s);
    1.46  fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
    1.47  
    1.48  end;
     2.1 --- a/src/Pure/System/isabelle_process.ML	Fri Aug 02 16:02:06 2013 +0200
     2.2 +++ b/src/Pure/System/isabelle_process.ML	Fri Aug 02 20:47:02 2013 +0200
     2.3 @@ -110,20 +110,17 @@
     2.4            ((case opt_serial of SOME i => cons (Markup.serialN, Markup.print_int i) | _ => I)
     2.5              (Position.properties_of (Position.thread_data ()))) body;
     2.6    in
     2.7 -    Output.Private_Hooks.status_fn := standard_message NONE Markup.statusN;
     2.8 -    Output.Private_Hooks.report_fn := standard_message NONE Markup.reportN;
     2.9 -    Output.Private_Hooks.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
    2.10 -    Output.Private_Hooks.writeln_fn :=
    2.11 -      (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
    2.12 -    Output.Private_Hooks.tracing_fn :=
    2.13 +    Output.Internal.status_fn := standard_message NONE Markup.statusN;
    2.14 +    Output.Internal.report_fn := standard_message NONE Markup.reportN;
    2.15 +    Output.Internal.result_fn := (fn (i, s) => standard_message (SOME i) Markup.resultN s);
    2.16 +    Output.Internal.writeln_fn := (fn s => standard_message (SOME (serial ())) Markup.writelnN s);
    2.17 +    Output.Internal.tracing_fn :=
    2.18        (fn s => (update_tracing (); standard_message (SOME (serial ())) Markup.tracingN s));
    2.19 -    Output.Private_Hooks.warning_fn :=
    2.20 -      (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    2.21 -    Output.Private_Hooks.error_fn :=
    2.22 -      (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    2.23 -    Output.Private_Hooks.protocol_message_fn := message Markup.protocolN;
    2.24 -    Output.Private_Hooks.urgent_message_fn := ! Output.Private_Hooks.writeln_fn;
    2.25 -    Output.Private_Hooks.prompt_fn := ignore;
    2.26 +    Output.Internal.warning_fn := (fn s => standard_message (SOME (serial ())) Markup.warningN s);
    2.27 +    Output.Internal.error_fn := (fn (i, s) => standard_message (SOME i) Markup.errorN s);
    2.28 +    Output.Internal.protocol_message_fn := message Markup.protocolN;
    2.29 +    Output.Internal.urgent_message_fn := ! Output.Internal.writeln_fn;
    2.30 +    Output.Internal.prompt_fn := ignore;
    2.31      message Markup.initN [] (Session.welcome ());
    2.32      msg_channel
    2.33    end;
     3.1 --- a/src/Pure/System/isar.ML	Fri Aug 02 16:02:06 2013 +0200
     3.2 +++ b/src/Pure/System/isar.ML	Fri Aug 02 20:47:02 2013 +0200
     3.3 @@ -156,7 +156,7 @@
     3.4  fun toplevel_loop in_stream {init = do_init, welcome, sync, secure} =
     3.5   (Context.set_thread_data NONE;
     3.6    if do_init then init () else ();
     3.7 -  Output.Private_Hooks.protocol_message_fn := protocol_message;
     3.8 +  Output.Internal.protocol_message_fn := protocol_message;
     3.9    if welcome then writeln (Session.welcome ()) else ();
    3.10    uninterruptible (fn _ => fn () => raw_loop secure (Outer_Syntax.isar in_stream sync)) ());
    3.11  
     4.1 --- a/src/Pure/Tools/build.ML	Fri Aug 02 16:02:06 2013 +0200
     4.2 +++ b/src/Pure/Tools/build.ML	Fri Aug 02 20:47:02 2013 +0200
     4.3 @@ -164,7 +164,7 @@
     4.4          theories |>
     4.5            (List.app (use_theories_condition last_timing)
     4.6              |> session_timing name verbose
     4.7 -            |> Unsynchronized.setmp Output.Private_Hooks.protocol_message_fn protocol_message
     4.8 +            |> Unsynchronized.setmp Output.Internal.protocol_message_fn protocol_message
     4.9              |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
    4.10              |> Exn.capture);
    4.11        val res2 = Exn.capture Session.finish ();
     5.1 --- a/src/Pure/Tools/proof_general.ML	Fri Aug 02 16:02:06 2013 +0200
     5.2 +++ b/src/Pure/Tools/proof_general.ML	Fri Aug 02 20:47:02 2013 +0200
     5.3 @@ -261,14 +261,14 @@
     5.4    | s => Output.physical_writeln (enclose bg en (prefix_lines prfx s)));
     5.5  
     5.6  fun setup_messages () =
     5.7 - (Output.Private_Hooks.writeln_fn := message "" "" "";
     5.8 -  Output.Private_Hooks.status_fn := (fn _ => ());
     5.9 -  Output.Private_Hooks.report_fn := (fn _ => ());
    5.10 -  Output.Private_Hooks.urgent_message_fn := message (special "I") (special "J") "";
    5.11 -  Output.Private_Hooks.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    5.12 -  Output.Private_Hooks.warning_fn := message (special "K") (special "L") "### ";
    5.13 -  Output.Private_Hooks.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    5.14 -  Output.Private_Hooks.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
    5.15 + (Output.Internal.writeln_fn := message "" "" "";
    5.16 +  Output.Internal.status_fn := (fn _ => ());
    5.17 +  Output.Internal.report_fn := (fn _ => ());
    5.18 +  Output.Internal.urgent_message_fn := message (special "I") (special "J") "";
    5.19 +  Output.Internal.tracing_fn := message (special "I" ^ special "V") (special "J") "";
    5.20 +  Output.Internal.warning_fn := message (special "K") (special "L") "### ";
    5.21 +  Output.Internal.error_fn := (fn (_, s) => message (special "M") (special "N") "*** " s);
    5.22 +  Output.Internal.prompt_fn := (fn s => Output.physical_stdout (render s ^ special "S")));
    5.23  
    5.24  
    5.25  (* notification *)