--- 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 *)