# HG changeset patch
# User wenzelm
# Date 1365515942 -7200
# Node ID 92e58b76dbb1e63a956cf5c6eae7bbfaaa17c238
# Parent  8e0a1d0a41ff028e0f62930846e5767cb2dcc73b
clarified protocol_message undefinedness;

diff -r 8e0a1d0a41ff -r 92e58b76dbb1 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Tue Apr 09 15:40:34 2013 +0200
+++ b/src/Pure/Concurrent/future.ML	Tue Apr 09 15:59:02 2013 +0200
@@ -203,10 +203,7 @@
         ("workers_active", Markup.print_int active),
         ("workers_waiting", Markup.print_int waiting)] @
         ML_Statistics.get ();
-    in
-      Output.protocol_message (Markup.ML_statistics :: stats) ""
-        handle Fail msg => warning msg
-    end
+    in Output.try_protocol_message (Markup.ML_statistics :: stats) "" end
   else ();
 
 
@@ -253,8 +250,7 @@
           fold (fn job => fn ok => job valid andalso ok) jobs true) ());
     val _ =
       if ! Multithreading.trace >= 2 then
-        Output.protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
-          handle Fail msg => warning msg
+        Output.try_protocol_message (Markup.task_statistics :: Task_Queue.task_statistics task) ""
       else ();
     val _ = SYNCHRONIZED "finish" (fn () =>
       let
diff -r 8e0a1d0a41ff -r 92e58b76dbb1 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Tue Apr 09 15:40:34 2013 +0200
+++ b/src/Pure/General/output.ML	Tue Apr 09 15:59:02 2013 +0200
@@ -24,6 +24,7 @@
   val physical_stdout: output -> unit
   val physical_stderr: output -> unit
   val physical_writeln: output -> unit
+  exception Protocol_Message of Properties.T
   structure Private_Hooks:
   sig
     val writeln_fn: (output -> unit) Unsynchronized.ref
@@ -45,6 +46,7 @@
   val report: string -> unit
   val result: serial * string -> unit
   val protocol_message: Properties.T -> string -> unit
+  val try_protocol_message: Properties.T -> string -> unit
 end;
 
 structure Output: OUTPUT =
@@ -88,6 +90,8 @@
 
 (* Isabelle output channels *)
 
+exception Protocol_Message of Properties.T;
+
 structure Private_Hooks =
 struct
   val writeln_fn = Unsynchronized.ref physical_writeln;
@@ -100,7 +104,7 @@
   val report_fn = Unsynchronized.ref (fn _: output => ());
   val result_fn = Unsynchronized.ref (fn _: serial * output => ());
   val protocol_message_fn: (Properties.T -> output -> unit) Unsynchronized.ref =
-    Unsynchronized.ref (fn _ => fn _ => raise Fail "Output.protocol_message undefined in TTY mode");
+    Unsynchronized.ref (fn props => fn _ => raise Protocol_Message props);
 end;
 
 fun writeln s = ! Private_Hooks.writeln_fn (output s);
@@ -114,6 +118,7 @@
 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 try_protocol_message props s = protocol_message props s handle Protocol_Message _ => ();
 
 end;
 
diff -r 8e0a1d0a41ff -r 92e58b76dbb1 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:40:34 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Apr 09 15:59:02 2013 +0200
@@ -656,10 +656,9 @@
       val _ =
         (case approximative_id tr of
           SOME id =>
-            (Output.protocol_message
+            (Output.try_protocol_message
               (Markup.command_timing ::
-                Markup.command_timing_properties id (#elapsed timing_result)) ""
-            handle Fail _ => ())
+                Markup.command_timing_properties id (#elapsed timing_result)) "")
         | NONE => ());
     in
       (result, Option.map (fn UNDEF => type_error tr state | exn => exn) opt_err)
diff -r 8e0a1d0a41ff -r 92e58b76dbb1 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue Apr 09 15:40:34 2013 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Apr 09 15:59:02 2013 +0200
@@ -265,7 +265,7 @@
   let
     val _ = kill_thy name;
     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
-    val _ = Output.protocol_message (Markup.loading_theory name) "" handle Fail _ => ();
+    val _ = Output.try_protocol_message (Markup.loading_theory name) "";
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
diff -r 8e0a1d0a41ff -r 92e58b76dbb1 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Apr 09 15:40:34 2013 +0200
+++ b/src/Pure/Tools/build.ML	Tue Apr 09 15:59:02 2013 +0200
@@ -14,15 +14,9 @@
 
 (* protocol messages *)
 
-local
-
 (* FIXME avoid hardwired stuff!? *)
 val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
 
-fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
-
-in
-
 fun protocol_message props output =
   (case props of
     function :: args =>
@@ -31,10 +25,8 @@
       else
         (case Markup.dest_loading_theory props of
           SOME name => writeln ("\floading_theory = " ^ name)
-        | NONE => protocol_undef ())
-  | [] => protocol_undef ());
-
-end;
+        | NONE => raise Output.Protocol_Message props)
+  | [] => raise Output.Protocol_Message props);
 
 
 (* build *)