equal
deleted
inserted
replaced
4 Build Isabelle sessions. |
4 Build Isabelle sessions. |
5 *) |
5 *) |
6 |
6 |
7 signature BUILD = |
7 signature BUILD = |
8 sig |
8 sig |
9 val build: string -> unit |
9 val build: string -> 'a |
10 end; |
10 end; |
11 |
11 |
12 structure Build: BUILD = |
12 structure Build: BUILD = |
13 struct |
13 struct |
14 |
14 |
53 " (undefined " ^ commas conds ^ ")\n")) |
53 " (undefined " ^ commas conds ^ ")\n")) |
54 end; |
54 end; |
55 |
55 |
56 in |
56 in |
57 |
57 |
58 fun build args_file = uninterruptible (fn restore_attributes => fn () => |
58 fun build args_file = Command_Line.tool (fn () => |
59 restore_attributes (fn () => |
|
60 let |
59 let |
61 val (do_output, (options, (verbose, (browser_info, (parent_name, |
60 val (do_output, (options, (verbose, (browser_info, (parent_name, |
62 (name, theories)))))) = |
61 (name, theories)))))) = |
63 File.read (Path.explode args_file) |> YXML.parse_body |> |
62 File.read (Path.explode args_file) |> YXML.parse_body |> |
64 let open XML.Decode in |
63 let open XML.Decode in |
81 (List.app use_theories |
80 (List.app use_theories |
82 |> Session.with_timing name verbose |
81 |> Session.with_timing name verbose |
83 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")); |
82 |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")); |
84 |
83 |
85 val _ = Session.finish (); |
84 val _ = Session.finish (); |
86 val _ = if do_output then () else quit (); |
85 val _ = if do_output then Secure.commit () else (); |
87 in () end) ()) () |
86 in 0 end); |
88 handle exn => |
|
89 (Output.error_msg (ML_Compiler.exn_message exn); |
|
90 if Exn.is_interrupt exn then exit 130 else exit 1); |
|
91 |
87 |
92 end; |
88 end; |
93 |
89 |
94 end; |
90 end; |