clarified protocol_message undefinedness;
authorwenzelm
Tue Apr 09 15:59:02 2013 +0200 (2013-04-09 ago)
changeset 5166192e58b76dbb1
parent 51660 8e0a1d0a41ff
child 51662 3391a493f39a
clarified protocol_message undefinedness;
src/Pure/Concurrent/future.ML
src/Pure/General/output.ML
src/Pure/Isar/toplevel.ML
src/Pure/Thy/thy_info.ML
src/Pure/Tools/build.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Apr 09 15:40:34 2013 +0200
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Apr 09 15:59:02 2013 +0200
     1.3 @@ -203,10 +203,7 @@
     1.4          ("workers_active", Markup.print_int active),
     1.5          ("workers_waiting", Markup.print_int waiting)] @
     1.6          ML_Statistics.get ();
     1.7 -    in
     1.8 -      Output.protocol_message (Markup.ML_statistics :: stats) ""
     1.9 -        handle Fail msg => warning msg
    1.10 -    end
    1.11 +    in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
    1.12    else ();
    1.13  
    1.14  
    1.15 @@ -253,8 +250,7 @@
    1.16            fold (fn job => fn ok => job valid andalso ok) jobs true) ());
    1.17      val _ =
    1.18        if ! Multithreading.trace >= 2 then
    1.19 -        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
    1.20 -          handle Fail msg => warning msg
    1.21 +        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
    1.22        else ();
    1.23      val _ = SYNCHRONIZED "finish" (fn () =>
    1.24        let
     2.1 --- a/src/Pure/General/output.ML	Tue Apr 09 15:40:34 2013 +0200
     2.2 +++ b/src/Pure/General/output.ML	Tue Apr 09 15:59:02 2013 +0200
     2.3 @@ -24,6 +24,7 @@
     2.4    val physical_stdout: output -> unit
     2.5    val physical_stderr: output -> unit
     2.6    val physical_writeln: output -> unit
     2.7 +  exception Protocol_Message of Properties.T
     2.8    structure Private_Hooks:
     2.9    sig
    2.10      val writeln_fn: (output -> unit) Unsynchronized.ref
    2.11 @@ -45,6 +46,7 @@
    2.12    val report: string -> unit
    2.13    val result: serial * string -> unit
    2.14    val protocol_message: Properties.T -> string -> unit
    2.15 +  val try_protocol_message: Properties.T -> string -> unit
    2.16  end;
    2.17  
    2.18  structure Output: OUTPUT =
    2.19 @@ -88,6 +90,8 @@
    2.20  
    2.21  (* Isabelle output channels *)
    2.22  
    2.23 +exception Protocol_Message of Properties.T;
    2.24 +
    2.25  structure Private_Hooks =
    2.26  struct
    2.27    val writeln_fn = Unsynchronized.ref physical_writeln;
    2.28 @@ -100,7 +104,7 @@
    2.29    val report_fn = Unsynchronized.ref (fn _: output => ());
    2.30    val result_fn = Unsynchronized.ref (fn _: serial * output => ());
    2.31    val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
    2.32 -    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
    2.33 +    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
    2.34  end;
    2.35  
    2.36  fun writeln s = ! Private_Hooks.writeln_fn (output s);
    2.37 @@ -114,6 +118,7 @@
    2.38  fun report s = ! Private_Hooks.report_fn (output s);
    2.39  fun result (i, s) = ! Private_Hooks.result_fn (i, output s);
    2.40  fun protocol_message props s = ! Private_Hooks.protocol_message_fn props (output s);
    2.41 +fun try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
    2.42  
    2.43  end;
    2.44  
     3.1 --- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:40:34 2013 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:59:02 2013 +0200
     3.3 @@ -656,10 +656,9 @@
     3.4        val _ =
     3.5          (case approximative_id tr of
     3.6            SOME id =>
     3.7 -            (Output.protocol_message
     3.8 +            (Output.try_protocol_message
     3.9                (Markup.command_timing ::
    3.10 -                Markup.command_timing_properties id (#elapsed timing_result)) ""
    3.11 -            handle Fail _ => ())
    3.12 +                Markup.command_timing_properties id (#elapsed timing_result)) "")
    3.13          | NONE => ());
    3.14      in
    3.15        (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
     4.1 --- a/src/Pure/Thy/thy_info.ML	Tue Apr 09 15:40:34 2013 +0200
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Tue Apr 09 15:59:02 2013 +0200
     4.3 @@ -265,7 +265,7 @@
     4.4    let
     4.5      val _ = kill_thy name;
     4.6      val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
     4.7 -    val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
     4.8 +    val _ = Output.try_protocol_message (Markup.loading_theory name) "";
     4.9  
    4.10      val {master = (thy_path, _), imports} = deps;
    4.11      val dir = Path.dir thy_path;
     5.1 --- a/src/Pure/Tools/build.ML	Tue Apr 09 15:40:34 2013 +0200
     5.2 +++ b/src/Pure/Tools/build.ML	Tue Apr 09 15:59:02 2013 +0200
     5.3 @@ -14,15 +14,9 @@
     5.4  
     5.5  (* protocol messages *)
     5.6  
     5.7 -local
     5.8 -
     5.9  (* FIXME avoid hardwired stuff!? *)
    5.10  val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    5.11  
    5.12 -fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    5.13 -
    5.14 -in
    5.15 -
    5.16  fun protocol_message props output =
    5.17    (case props of
    5.18      function :: args =>
    5.19 @@ -31,10 +25,8 @@
    5.20        else
    5.21          (case Markup.dest_loading_theory props of
    5.22            SOME name => writeln ("\floading_theory = " ^ name)
    5.23 -        | NONE => protocol_undef ())
    5.24 -  | [] => protocol_undef ());
    5.25 -
    5.26 -end;
    5.27 +        | NONE => raise Output.Protocol_Message props)
    5.28 +  | [] => raise Output.Protocol_Message props);
    5.29  
    5.30  
    5.31  (* build *)