54 |
54 |
55 in |
55 in |
56 |
56 |
57 fun build args_file = |
57 fun build args_file = |
58 let |
58 let |
59 val (do_output, (options, (timing, (verbose, (browser_info, (parent_base_name, |
59 val (do_output, (options, (timing, (verbose, (browser_info, (parent_name, |
60 (name, (base_name, theories)))))))) = |
60 (name, theories))))))) = |
61 File.read (Path.explode args_file) |> YXML.parse_body |> |
61 File.read (Path.explode args_file) |> YXML.parse_body |> |
62 let open XML.Decode in |
62 let open XML.Decode in |
63 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string |
63 pair bool (pair Options.decode (pair bool (pair bool (pair string (pair string |
64 (pair string (pair string ((list (pair Options.decode (list string))))))))))) |
64 (pair string ((list (pair Options.decode (list string)))))))))) |
65 end; |
65 end; |
66 |
66 |
67 val _ = |
67 val _ = |
68 Session.init do_output false |
68 Session.init do_output false |
69 (Options.bool options "browser_info") browser_info |
69 (Options.bool options "browser_info") browser_info |
70 (Options.string options "document") |
70 (Options.string options "document") |
71 (Options.bool options "document_graph") |
71 (Options.bool options "document_graph") |
72 (space_explode ":" (Options.string options "document_variants")) |
72 (space_explode ":" (Options.string options "document_variants")) |
73 parent_base_name base_name |
73 parent_name name |
74 (Options.string options "document_dump", Options.string options "document_dump_mode") |
74 (Options.string options "document_dump", Options.string options "document_dump_mode") |
75 "" verbose; |
75 "" verbose; |
76 val _ = Session.with_timing name timing (List.app use_theories) theories; |
76 val _ = Session.with_timing name timing (List.app use_theories) theories; |
77 val _ = Session.finish (); |
77 val _ = Session.finish (); |
78 val _ = if do_output then () else quit (); |
78 val _ = if do_output then () else quit (); |