src/Pure/Tools/build.ML
changeset 51216 e6e7685fc8f8
parent 51045 630c0895d9d1
child 51217 65ab2c4f4c32
     1.1 --- a/src/Pure/Tools/build.ML	Mon Feb 18 18:34:55 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Tue Feb 19 10:55:11 2013 +0100
     1.3 @@ -16,30 +16,23 @@
     1.4  
     1.5  local
     1.6  
     1.7 -fun ML_statistics (function :: stats) "" =
     1.8 -      if function = Markup.ML_statistics then SOME stats
     1.9 -      else NONE
    1.10 -  | ML_statistics _ _ = NONE;
    1.11 +(* FIXME avoid hardwired stuff!? *)
    1.12 +val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    1.13  
    1.14 -fun task_statistics (function :: stats) "" =
    1.15 -      if function = Markup.task_statistics then SOME stats
    1.16 -      else NONE
    1.17 -  | task_statistics _ _ = NONE;
    1.18 -
    1.19 -val print_properties = YXML.string_of_body o XML.Encode.properties;
    1.20 +fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
    1.21  
    1.22  in
    1.23  
    1.24  fun protocol_message props output =
    1.25 -  (case ML_statistics props output of
    1.26 -    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
    1.27 -  | NONE =>
    1.28 -      (case task_statistics props output of
    1.29 -        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
    1.30 -      | NONE =>
    1.31 -          (case Markup.dest_loading_theory props of
    1.32 -            SOME name => writeln ("\floading_theory = " ^ name)
    1.33 -          | NONE => raise Fail "Undefined Output.protocol_message")));
    1.34 +  (case props of
    1.35 +    function :: args =>
    1.36 +      if member (op =) protocol_echo function then
    1.37 +        writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    1.38 +      else
    1.39 +        (case Markup.dest_loading_theory props of
    1.40 +          SOME name => writeln ("\floading_theory = " ^ name)
    1.41 +        | NONE => protocol_undef ())
    1.42 +  | [] => protocol_undef ());
    1.43  
    1.44  end;
    1.45