121 |
121 |
122 fun build args_file = Command_Line.tool0 (fn () => |
122 fun build args_file = Command_Line.tool0 (fn () => |
123 let |
123 let |
124 val _ = SHA1_Samples.test (); |
124 val _ = SHA1_Samples.test (); |
125 |
125 |
126 val (command_timings, (do_output, (options, (verbose, (browser_info, |
126 val (symbol_codes, (command_timings, (do_output, (options, (verbose, (browser_info, |
127 (document_files, (graph_file, (parent_name, (chapter, (name, theories)))))))))) = |
127 (document_files, (graph_file, (parent_name, (chapter, (name, theories))))))))))) = |
128 File.read (Path.explode args_file) |> YXML.parse_body |> |
128 File.read (Path.explode args_file) |> YXML.parse_body |> |
129 let open XML.Decode in |
129 let open XML.Decode in |
130 pair (list properties) (pair bool (pair Options.decode (pair bool (pair string |
130 pair (list (pair string int)) (pair (list properties) (pair bool (pair Options.decode |
131 (pair (list (pair string string)) (pair string (pair string (pair string (pair string |
131 (pair bool (pair string (pair (list (pair string string)) (pair string |
132 ((list (pair Options.decode (list (string #> rpair Position.none)))))))))))))) |
132 (pair string (pair string (pair string |
|
133 ((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))) |
133 end; |
134 end; |
134 |
135 |
|
136 val _ = HTML.init_symbols symbol_codes; |
135 val _ = Options.set_default options; |
137 val _ = Options.set_default options; |
136 |
138 |
137 val _ = writeln ("\fSession.name = " ^ name); |
139 val _ = writeln ("\fSession.name = " ^ name); |
138 val _ = |
140 val _ = |
139 Session.init do_output |
141 Session.init do_output |
157 |> Multithreading.max_threads_setmp (Options.int options "threads") |
159 |> Multithreading.max_threads_setmp (Options.int options "threads") |
158 |> Exn.capture); |
160 |> Exn.capture); |
159 val res2 = Exn.capture Session.finish (); |
161 val res2 = Exn.capture Session.finish (); |
160 val _ = Par_Exn.release_all [res1, res2]; |
162 val _ = Par_Exn.release_all [res1, res2]; |
161 |
163 |
|
164 val _ = HTML.reset_symbols (); |
162 val _ = Options.reset_default (); |
165 val _ = Options.reset_default (); |
163 val _ = if do_output then () else exit 0; |
166 val _ = if do_output then () else exit 0; |
164 in () end); |
167 in () end); |
165 |
168 |
166 |
169 |