src/Pure/Tools/build.ML
changeset 51045 630c0895d9d1
parent 50982 a7aa17a1f721
child 51216 e6e7685fc8f8
     1.1 --- a/src/Pure/Tools/build.ML	Tue Jan 22 11:28:54 2013 +0100
     1.2 +++ b/src/Pure/Tools/build.ML	Thu Jan 24 17:18:13 2013 +0100
     1.3 @@ -14,6 +14,8 @@
     1.4  
     1.5  (* protocol messages *)
     1.6  
     1.7 +local
     1.8 +
     1.9  fun ML_statistics (function :: stats) "" =
    1.10        if function = Markup.ML_statistics then SOME stats
    1.11        else NONE
    1.12 @@ -24,17 +26,23 @@
    1.13        else NONE
    1.14    | task_statistics _ _ = NONE;
    1.15  
    1.16 +val print_properties = YXML.string_of_body o XML.Encode.properties;
    1.17 +
    1.18 +in
    1.19 +
    1.20  fun protocol_message props output =
    1.21    (case ML_statistics props output of
    1.22 -    SOME stats => writeln ("\fML_statistics = " ^ ML_Syntax.print_properties stats)
    1.23 +    SOME stats => writeln ("\fML_statistics = " ^ print_properties stats)
    1.24    | NONE =>
    1.25        (case task_statistics props output of
    1.26 -        SOME stats => writeln ("\ftask_statistics = " ^ ML_Syntax.print_properties stats)
    1.27 +        SOME stats => writeln ("\ftask_statistics = " ^ print_properties stats)
    1.28        | NONE =>
    1.29            (case Markup.dest_loading_theory props of
    1.30              SOME name => writeln ("\floading_theory = " ^ name)
    1.31            | NONE => raise Fail "Undefined Output.protocol_message")));
    1.32  
    1.33 +end;
    1.34 +
    1.35  
    1.36  (* build *)
    1.37