equal
deleted
inserted
replaced
222 new Session(options, resources) { |
222 new Session(options, resources) { |
223 override val xml_cache: XML.Cache = store.xml_cache |
223 override val xml_cache: XML.Cache = store.xml_cache |
224 override val xz_cache: XZ.Cache = store.xz_cache |
224 override val xz_cache: XZ.Cache = store.xz_cache |
225 } |
225 } |
226 |
226 |
227 val build_session_errors: Promise[List[String]] = Future.promise |
227 object Build_Session_Errors |
|
228 { |
|
229 private val promise: Promise[List[String]] = Future.promise |
|
230 |
|
231 def result: Exn.Result[List[String]] = promise.join_result |
|
232 def cancel: Unit = promise.cancel |
|
233 def apply(errs: List[String]) |
|
234 { |
|
235 try { promise.fulfill(errs) } |
|
236 catch { case _: IllegalStateException => } |
|
237 } |
|
238 } |
|
239 |
228 val stdout = new StringBuilder(1000) |
240 val stdout = new StringBuilder(1000) |
229 val stderr = new StringBuilder(1000) |
241 val stderr = new StringBuilder(1000) |
230 val messages = new mutable.ListBuffer[XML.Elem] |
242 val messages = new mutable.ListBuffer[XML.Elem] |
231 val command_timings = new mutable.ListBuffer[Properties.T] |
243 val command_timings = new mutable.ListBuffer[Properties.T] |
232 val theory_timings = new mutable.ListBuffer[Properties.T] |
244 val theory_timings = new mutable.ListBuffer[Properties.T] |
246 }) |
258 }) |
247 } |
259 } |
248 |
260 |
249 session.init_protocol_handler(new Session.Protocol_Handler |
261 session.init_protocol_handler(new Session.Protocol_Handler |
250 { |
262 { |
251 override def exit() { build_session_errors.cancel } |
263 override def exit() { Build_Session_Errors.cancel } |
252 |
264 |
253 private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
265 private def build_session_finished(msg: Prover.Protocol_Output): Boolean = |
254 { |
266 { |
255 val (rc, errors) = |
267 val (rc, errors) = |
256 try { |
268 try { |
267 (rc, errors) |
279 (rc, errors) |
268 } |
280 } |
269 catch { case ERROR(err) => (2, List(err)) } |
281 catch { case ERROR(err) => (2, List(err)) } |
270 |
282 |
271 session.protocol_command("Prover.stop", rc.toString) |
283 session.protocol_command("Prover.stop", rc.toString) |
272 try { build_session_errors.fulfill(errors) } |
284 Build_Session_Errors(errors) |
273 catch { case _ : IllegalStateException => } |
|
274 true |
285 true |
275 } |
286 } |
276 |
287 |
277 private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
288 private def loading_theory(msg: Prover.Protocol_Output): Boolean = |
278 msg.properties match { |
289 msg.properties match { |
320 "Prover terminated" + |
331 "Prover terminated" + |
321 (msg.properties match { |
332 (msg.properties match { |
322 case Markup.Process_Result(result) => ": " + result.print_rc |
333 case Markup.Process_Result(result) => ": " + result.print_rc |
323 case _ => "" |
334 case _ => "" |
324 }) |
335 }) |
325 try { build_session_errors.fulfill(List(err)) } |
336 Build_Session_Errors(List(err)) |
326 catch { case _ : IllegalStateException => } |
|
327 } |
337 } |
328 case _ => |
338 case _ => |
329 } |
339 } |
330 |
340 |
331 val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
341 val eval_main = Command_Line.ML_tool("Isabelle_Process.init_build ()" :: eval_store) |
339 val errors = |
349 val errors = |
340 Isabelle_Thread.interrupt_handler(_ => process.terminate) { |
350 Isabelle_Thread.interrupt_handler(_ => process.terminate) { |
341 Exn.capture { process.await_startup } match { |
351 Exn.capture { process.await_startup } match { |
342 case Exn.Res(_) => |
352 case Exn.Res(_) => |
343 session.protocol_command("build_session", args_yxml) |
353 session.protocol_command("build_session", args_yxml) |
344 build_session_errors.join_result |
354 Build_Session_Errors.result |
345 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
355 case Exn.Exn(exn) => Exn.Res(List(Exn.message(exn))) |
346 } |
356 } |
347 } |
357 } |
348 |
358 |
349 val process_result = |
359 val process_result = |