src/Pure/Tools/build.ML
changeset 53212 387b9f7cb0ac
parent 52852 08ecbffaf25c
child 54458 96ccc8972fc7
equal deleted inserted replaced
53211:753b9fbe18be 53212:387b9f7cb0ac
   125 
   125 
   126 in
   126 in
   127 
   127 
   128 fun build args_file = Command_Line.tool (fn () =>
   128 fun build args_file = Command_Line.tool (fn () =>
   129     let
   129     let
       
   130       val _ = SHA1_Samples.test ();
       
   131 
   130       val (command_timings, (do_output, (options, (verbose, (browser_info,
   132       val (command_timings, (do_output, (options, (verbose, (browser_info,
   131           (parent_name, (chapter, (name, theories)))))))) =
   133           (parent_name, (chapter, (name, theories)))))))) =
   132         File.read (Path.explode args_file) |> YXML.parse_body |>
   134         File.read (Path.explode args_file) |> YXML.parse_body |>
   133           let open XML.Decode in
   135           let open XML.Decode in
   134             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
   136             pair (list properties) (pair bool (pair Options.decode (pair bool (pair string