src/Pure/Tools/build.ML
changeset 56533 cd8b6d849b6a
parent 56530 5c178501cf78
child 56612 74851ff86180
     1.1 --- a/src/Pure/Tools/build.ML	Fri Apr 11 09:36:38 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.ML	Fri Apr 11 11:52:28 2014 +0200
     1.3 @@ -130,12 +130,12 @@
     1.4        val _ = SHA1_Samples.test ();
     1.5  
     1.6        val (command_timings, (do_output, (options, (verbose, (browser_info,
     1.7 -          (parent_name, (chapter, (name, theories)))))))) =
     1.8 +          (document_files, (parent_name, (chapter, (name, theories))))))))) =
     1.9          File.read (Path.explode args_file) |> YXML.parse_body |>
    1.10            let open XML.Decode in
    1.11              pair (list properties) (pair bool (pair Options.decode (pair bool (pair string
    1.12 -              (pair string (pair string (pair string
    1.13 -                ((list (pair Options.decode (list string)))))))))))
    1.14 +              (pair (list (pair string string)) (pair string (pair string (pair string
    1.15 +                ((list (pair Options.decode (list string))))))))))))
    1.16            end;
    1.17  
    1.18        val _ = Options.set_default options;
    1.19 @@ -156,6 +156,7 @@
    1.20            (Options.bool options "document_graph")
    1.21            (Options.string options "document_output")
    1.22            document_variants
    1.23 +          (map (pairself Path.explode) document_files)
    1.24            parent_name (chapter, name)
    1.25            verbose;
    1.26