95 | [] => raise Output.Protocol_Message props); |
95 | [] => raise Output.Protocol_Message props); |
96 |
96 |
97 |
97 |
98 (* build *) |
98 (* build *) |
99 |
99 |
|
100 fun build_theories last_timing master_dir (options, thys) = |
|
101 let |
|
102 val condition = space_explode "," (Options.string options "condition"); |
|
103 val conds = filter_out (can getenv_strict) condition; |
|
104 in |
|
105 if null conds then |
|
106 (Options.set_default options; |
|
107 (Thy_Info.use_theories { |
|
108 document = Present.document_enabled (Options.string options "document"), |
|
109 last_timing = last_timing, |
|
110 master_dir = master_dir} |
|
111 |> Unsynchronized.setmp print_mode |
|
112 (space_explode "," (Options.string options "print_mode") @ print_mode_value ()) |
|
113 |> Unsynchronized.setmp Goal.parallel_proofs (Options.int options "parallel_proofs") |
|
114 |> Unsynchronized.setmp Multithreading.trace (Options.int options "threads_trace") |
|
115 |> Multithreading.max_threads_setmp (Options.int options "threads") |
|
116 |> Unsynchronized.setmp Future.ML_statistics true) thys) |
|
117 else |
|
118 Output.physical_stderr ("Skipping theories " ^ commas_quote (map #1 thys) ^ |
|
119 " (undefined " ^ commas conds ^ ")\n") |
|
120 end; |
|
121 |
100 fun build args_file = Command_Line.tool0 (fn () => |
122 fun build args_file = Command_Line.tool0 (fn () => |
101 let |
123 let |
102 val _ = SHA1_Samples.test (); |
124 val _ = SHA1_Samples.test (); |
103 |
125 |
104 val (command_timings, (do_output, (options, (verbose, (browser_info, |
126 val (command_timings, (do_output, (options, (verbose, (browser_info, |
127 |
149 |
128 val last_timing = lookup_timings (fold update_timings command_timings empty_timings); |
150 val last_timing = lookup_timings (fold update_timings command_timings empty_timings); |
129 |
151 |
130 val res1 = |
152 val res1 = |
131 theories |> |
153 theories |> |
132 (List.app (Thy_Info.build_theories last_timing Path.current) |
154 (List.app (build_theories last_timing Path.current) |
133 |> session_timing name verbose |
155 |> session_timing name verbose |
134 |> Unsynchronized.setmp Output.protocol_message_fn protocol_message |
156 |> Unsynchronized.setmp Output.protocol_message_fn protocol_message |
135 |> Multithreading.max_threads_setmp (Options.int options "threads") |
157 |> Multithreading.max_threads_setmp (Options.int options "threads") |
136 |> Exn.capture); |
158 |> Exn.capture); |
137 val res2 = Exn.capture Session.finish (); |
159 val res2 = Exn.capture Session.finish (); |
139 |
161 |
140 val _ = Options.reset_default (); |
162 val _ = Options.reset_default (); |
141 val _ = if do_output then () else exit 0; |
163 val _ = if do_output then () else exit 0; |
142 in () end); |
164 in () end); |
143 |
165 |
|
166 |
|
167 (* PIDE protocol *) |
|
168 |
|
169 val _ = |
|
170 Isabelle_Process.protocol_command "build_theories" |
|
171 (fn [id, master_dir, theories_yxml] => |
|
172 let |
|
173 val theories = |
|
174 YXML.parse_body theories_yxml |> |
|
175 let open XML.Decode |
|
176 in list (pair Options.decode (list (string #> rpair Position.none))) end; |
|
177 val result = |
|
178 Exn.capture (fn () => |
|
179 theories |> List.app (build_theories (K NONE) (Path.explode master_dir))) (); |
|
180 val ok = |
|
181 (case result of |
|
182 Exn.Res _ => true |
|
183 | Exn.Exn exn => (Runtime.exn_error_message exn; false)); |
|
184 in Output.protocol_message (Markup.build_theories_result id ok) [] end); |
|
185 |
144 end; |
186 end; |