equal
deleted
inserted
replaced
12 structure Build: BUILD = |
12 structure Build: BUILD = |
13 struct |
13 struct |
14 |
14 |
15 fun build args_file = |
15 fun build args_file = |
16 let |
16 let |
17 val (build_images, (parent, (name, theories))) = |
17 val (save, (parent, (name, theories))) = |
18 File.read (Path.explode args_file) |> YXML.parse_body |> |
18 File.read (Path.explode args_file) |> YXML.parse_body |> |
19 let open XML.Decode in pair bool (pair string (pair string (list string))) end; |
19 let open XML.Decode in pair bool (pair string (pair string (list string))) end; |
20 |
20 |
21 val _ = Session.init false parent name; (* FIXME reset!? *) |
21 val _ = Session.init false parent name; (* FIXME reset!? *) |
22 val _ = Thy_Info.use_thys theories; |
22 val _ = Thy_Info.use_thys theories; |
23 val _ = Session.finish (); |
23 val _ = Session.finish (); |
24 |
24 |
25 val _ = if build_images then () else quit (); |
25 val _ = if save then () else quit (); |
26 in () end |
26 in () end |
27 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); |
27 handle exn => (Output.error_msg (ML_Compiler.exn_message exn); exit 1); |
28 |
28 |
29 end; |
29 end; |