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