src/Pure/Tools/build.ML
changeset 51661 92e58b76dbb1
parent 51553 63327f679cff
child 51662 3391a493f39a
     1.1 --- a/src/Pure/Tools/build.ML	Tue Apr 09 15:40:34 2013 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Apr 09 15:59:02 2013 +0200
     1.3 @@ -14,15 +14,9 @@
     1.4  
     1.5  (* protocol messages *)
     1.6  
     1.7 -local
     1.8 -
     1.9  (* FIXME avoid hardwired stuff!? *)
    1.10  val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    1.11  
    1.12 -fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    1.13 -
    1.14 -in
    1.15 -
    1.16  fun protocol_message props output =
    1.17    (case props of
    1.18      function :: args =>
    1.19 @@ -31,10 +25,8 @@
    1.20        else
    1.21          (case Markup.dest_loading_theory props of
    1.22            SOME name => writeln ("\floading_theory = " ^ name)
    1.23 -        | NONE => protocol_undef ())
    1.24 -  | [] => protocol_undef ());
    1.25 -
    1.26 -end;
    1.27 +        | NONE => raise Output.Protocol_Message props)
    1.28 +  | [] => raise Output.Protocol_Message props);
    1.29  
    1.30  
    1.31  (* build *)