341 prover.get.update(previous.id, version.id, doc_edits) |
341 prover.get.update(previous.id, version.id, doc_edits) |
342 } |
342 } |
343 //}}} |
343 //}}} |
344 |
344 |
345 |
345 |
346 /* prover results */ |
346 /* prover output */ |
347 |
347 |
348 def handle_result(result: Isabelle_Process.Result) |
348 def handle_output(output: Isabelle_Process.Output) |
349 //{{{ |
349 //{{{ |
350 { |
350 { |
351 def bad_result(result: Isabelle_Process.Result) |
351 def bad_output(output: Isabelle_Process.Output) |
352 { |
352 { |
353 if (verbose) |
353 if (verbose) |
354 System.err.println("Ignoring prover result: " + result.message.toString) |
354 System.err.println("Ignoring prover output: " + output.message.toString) |
355 } |
355 } |
356 |
356 |
357 result.properties match { |
357 output.properties match { |
358 |
358 |
359 case Position.Id(state_id) if !result.is_raw => |
359 case Position.Id(state_id) if !output.is_raw => |
360 try { |
360 try { |
361 val st = global_state >>> (_.accumulate(state_id, result.message)) |
361 val st = global_state >>> (_.accumulate(state_id, output.message)) |
362 delay_commands_changed.invoke(st.command) |
362 delay_commands_changed.invoke(st.command) |
363 } |
363 } |
364 catch { |
364 catch { |
365 case _: Document.State.Fail => bad_result(result) |
365 case _: Document.State.Fail => bad_output(output) |
366 } |
366 } |
367 |
367 |
368 case Isabelle_Markup.Assign_Execs if result.is_raw => |
368 case Isabelle_Markup.Assign_Execs if output.is_raw => |
369 XML.content(result.body).mkString match { |
369 XML.content(output.body).mkString match { |
370 case Protocol.Assign(id, assign) => |
370 case Protocol.Assign(id, assign) => |
371 try { handle_assign(id, assign) } |
371 try { handle_assign(id, assign) } |
372 catch { case _: Document.State.Fail => bad_result(result) } |
372 catch { case _: Document.State.Fail => bad_output(output) } |
373 case _ => bad_result(result) |
373 case _ => bad_output(output) |
374 } |
374 } |
375 // FIXME separate timeout event/message!? |
375 // FIXME separate timeout event/message!? |
376 if (prover.isDefined && System.currentTimeMillis() > prune_next) { |
376 if (prover.isDefined && System.currentTimeMillis() > prune_next) { |
377 val old_versions = global_state >>> (_.prune_history(prune_size)) |
377 val old_versions = global_state >>> (_.prune_history(prune_size)) |
378 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) |
378 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions) |
379 prune_next = System.currentTimeMillis() + prune_delay.ms |
379 prune_next = System.currentTimeMillis() + prune_delay.ms |
380 } |
380 } |
381 |
381 |
382 case Isabelle_Markup.Removed_Versions if result.is_raw => |
382 case Isabelle_Markup.Removed_Versions if output.is_raw => |
383 XML.content(result.body).mkString match { |
383 XML.content(output.body).mkString match { |
384 case Protocol.Removed(removed) => |
384 case Protocol.Removed(removed) => |
385 try { handle_removed(removed) } |
385 try { handle_removed(removed) } |
386 catch { case _: Document.State.Fail => bad_result(result) } |
386 catch { case _: Document.State.Fail => bad_output(output) } |
387 case _ => bad_result(result) |
387 case _ => bad_output(output) |
388 } |
388 } |
389 |
389 |
390 case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw => |
390 case Isabelle_Markup.Invoke_Scala(name, id) if output.is_raw => |
391 Future.fork { |
391 Future.fork { |
392 val arg = XML.content(result.body).mkString |
392 val arg = XML.content(output.body).mkString |
393 val (tag, res) = Invoke_Scala.method(name, arg) |
393 val (tag, res) = Invoke_Scala.method(name, arg) |
394 prover.get.invoke_scala(id, tag, res) |
394 prover.get.invoke_scala(id, tag, res) |
395 } |
395 } |
396 |
396 |
397 case Isabelle_Markup.Cancel_Scala(id) if result.is_raw => |
397 case Isabelle_Markup.Cancel_Scala(id) if output.is_raw => |
398 System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task |
398 System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task |
399 |
399 |
400 case Isabelle_Markup.Ready if result.is_raw => |
400 case Isabelle_Markup.Ready if output.is_raw => |
401 // FIXME move to ML side (!?) |
401 // FIXME move to ML side (!?) |
402 syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have") |
402 syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have") |
403 syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show") |
403 syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show") |
404 phase = Session.Ready |
404 phase = Session.Ready |
405 |
405 |
406 case Isabelle_Markup.Loaded_Theory(name) if result.is_raw => |
406 case Isabelle_Markup.Loaded_Theory(name) if output.is_raw => |
407 thy_load.register_thy(name) |
407 thy_load.register_thy(name) |
408 |
408 |
409 case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw => |
409 case Isabelle_Markup.Command_Decl(name, kind) if output.is_raw => |
410 syntax += (name, kind) |
410 syntax += (name, kind) |
411 |
411 |
412 case Isabelle_Markup.Keyword_Decl(name) if result.is_raw => |
412 case Isabelle_Markup.Keyword_Decl(name) if output.is_raw => |
413 syntax += name |
413 syntax += name |
414 |
414 |
415 case _ => |
415 case _ => |
416 if (result.is_exit && phase == Session.Startup) phase = Session.Failed |
416 if (output.is_exit && phase == Session.Startup) phase = Session.Failed |
417 else if (result.is_exit) phase = Session.Inactive |
417 else if (output.is_exit) phase = Session.Inactive |
418 else if (result.is_stdout) { } |
418 else if (output.is_stdout) { } |
419 else bad_result(result) |
419 else bad_output(output) |
420 } |
420 } |
421 } |
421 } |
422 //}}} |
422 //}}} |
423 |
423 |
424 |
424 |
471 case Messages(msgs) => |
471 case Messages(msgs) => |
472 msgs foreach { |
472 msgs foreach { |
473 case input: Isabelle_Process.Input => |
473 case input: Isabelle_Process.Input => |
474 protocol_messages.event(input) |
474 protocol_messages.event(input) |
475 |
475 |
476 case result: Isabelle_Process.Result => |
476 case output: Isabelle_Process.Output => |
477 handle_result(result) |
477 handle_output(output) |
478 if (result.is_syslog) syslog_messages.event(result) |
478 if (output.is_syslog) syslog_messages.event(output) |
479 if (result.is_stdout || result.is_stderr) raw_output_messages.event(result) |
479 if (output.is_stdout || output.is_stderr) raw_output_messages.event(output) |
480 protocol_messages.event(result) |
480 protocol_messages.event(output) |
481 } |
481 } |
482 |
482 |
483 case change: Change_Node |
483 case change: Change_Node |
484 if prover.isDefined && global_state().is_assigned(change.previous) => |
484 if prover.isDefined && global_state().is_assigned(change.previous) => |
485 handle_change(change) |
485 handle_change(change) |