src/Pure/Tools/build.ML
changeset 51661 92e58b76dbb1
parent 51553 63327f679cff
child 51662 3391a493f39a
equal deleted inserted replaced
51660:8e0a1d0a41ff 51661:92e58b76dbb1
    12 structure Build: BUILD =
    12 structure Build: BUILD =
    13 struct
    13 struct
    14 
    14 
    15 (* protocol messages *)
    15 (* protocol messages *)
    16 
    16 
    17 local
       
    18 
       
    19 (* FIXME avoid hardwired stuff!? *)
    17 (* FIXME avoid hardwired stuff!? *)
    20 val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    18 val protocol_echo = [Markup.ML_statistics, Markup.task_statistics, Markup.command_timing];
    21 
       
    22 fun protocol_undef () = raise Fail "Undefined Output.protocol_message";
       
    23 
       
    24 in
       
    25 
    19 
    26 fun protocol_message props output =
    20 fun protocol_message props output =
    27   (case props of
    21   (case props of
    28     function :: args =>
    22     function :: args =>
    29       if member (op =) protocol_echo function then
    23       if member (op =) protocol_echo function then
    30         writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    24         writeln ("\f" ^ #2 function ^ " = " ^ YXML.string_of_body (XML.Encode.properties args))
    31       else
    25       else
    32         (case Markup.dest_loading_theory props of
    26         (case Markup.dest_loading_theory props of
    33           SOME name => writeln ("\floading_theory = " ^ name)
    27           SOME name => writeln ("\floading_theory = " ^ name)
    34         | NONE => protocol_undef ())
    28         | NONE => raise Output.Protocol_Message props)
    35   | [] => protocol_undef ());
    29   | [] => raise Output.Protocol_Message props);
    36 
       
    37 end;
       
    38 
    30 
    39 
    31 
    40 (* build *)
    32 (* build *)
    41 
    33 
    42 local
    34 local