189 |
189 |
190 private case class Start(start_prover: Prover.Receiver => Prover) |
190 private case class Start(start_prover: Prover.Receiver => Prover) |
191 private case object Stop |
191 private case object Stop |
192 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
192 private case class Cancel_Exec(exec_id: Document_ID.Exec) |
193 private case class Protocol_Command(name: String, args: List[String]) |
193 private case class Protocol_Command(name: String, args: List[String]) |
|
194 private case class Add_Export(args: Markup.Export.Args, bytes: Bytes, output: Prover.Output) |
194 private case class Update_Options(options: Options) |
195 private case class Update_Options(options: Options) |
195 private case object Consolidate_Execution |
196 private case object Consolidate_Execution |
196 private case object Prune_History |
197 private case object Prune_History |
197 |
198 |
198 |
199 |
398 //}}} |
399 //}}} |
399 |
400 |
400 |
401 |
401 /* prover output */ |
402 /* prover output */ |
402 |
403 |
|
404 def bad_output(output: Prover.Output) |
|
405 { |
|
406 if (verbose) |
|
407 Output.warning("Ignoring bad prover output: " + output.message.toString) |
|
408 } |
|
409 |
|
410 def change_command(f: Document.State => (Command.State, Document.State), output: Prover.Output) |
|
411 { |
|
412 try { |
|
413 val st = global_state.change_result(f) |
|
414 change_buffer.invoke(false, List(st.command)) |
|
415 } |
|
416 catch { case _: Document.State.Fail => bad_output(output) } |
|
417 } |
|
418 |
403 def handle_output(output: Prover.Output) |
419 def handle_output(output: Prover.Output) |
404 //{{{ |
420 //{{{ |
405 { |
421 { |
406 def bad_output() |
422 def accumulate(state_id: Document_ID.Generic, message: XML.Elem): Unit = |
407 { |
423 change_command(_.accumulate(state_id, message, xml_cache), output) |
408 if (verbose) |
|
409 Output.warning("Ignoring bad prover output: " + output.message.toString) |
|
410 } |
|
411 |
|
412 def accumulate(state_id: Document_ID.Generic, message: XML.Elem) |
|
413 { |
|
414 try { |
|
415 val st = global_state.change_result(_.accumulate(state_id, message, xml_cache)) |
|
416 change_buffer.invoke(false, List(st.command)) |
|
417 } |
|
418 catch { |
|
419 case _: Document.State.Fail => bad_output() |
|
420 } |
|
421 } |
|
422 |
424 |
423 output match { |
425 output match { |
424 case msg: Prover.Protocol_Output => |
426 case msg: Prover.Protocol_Output => |
425 val handled = protocol_handlers.invoke(msg) |
427 val handled = protocol_handlers.invoke(msg) |
426 if (!handled) { |
428 if (!handled) { |
433 accumulate(state_id, xml_cache.elem(message)) |
435 accumulate(state_id, xml_cache.elem(message)) |
434 |
436 |
435 case Protocol.Theory_Timing(_, _) => |
437 case Protocol.Theory_Timing(_, _) => |
436 // FIXME |
438 // FIXME |
437 |
439 |
438 case Markup.Export(_) => |
440 case Markup.Export(args) |
439 // FIXME |
441 if args.id.isDefined && Value.Long.unapply(args.id.get).isDefined => |
|
442 if (args.compress) { |
|
443 Future.fork { manager.send(Add_Export(args, msg.bytes.compress(), output)) } |
|
444 } |
|
445 else manager.send(Add_Export(args, msg.bytes, output)) |
440 |
446 |
441 case Markup.Assign_Update => |
447 case Markup.Assign_Update => |
442 msg.text match { |
448 msg.text match { |
443 case Protocol.Assign_Update(id, update) => |
449 case Protocol.Assign_Update(id, update) => |
444 try { |
450 try { |
445 val cmds = global_state.change_result(_.assign(id, update)) |
451 val cmds = global_state.change_result(_.assign(id, update)) |
446 change_buffer.invoke(true, cmds) |
452 change_buffer.invoke(true, cmds) |
447 manager.send(Session.Change_Flush) |
453 manager.send(Session.Change_Flush) |
448 } |
454 } |
449 catch { case _: Document.State.Fail => bad_output() } |
455 catch { case _: Document.State.Fail => bad_output(output) } |
450 case _ => bad_output() |
456 case _ => bad_output(output) |
451 } |
457 } |
452 delay_prune.invoke() |
458 delay_prune.invoke() |
453 |
459 |
454 case Markup.Removed_Versions => |
460 case Markup.Removed_Versions => |
455 msg.text match { |
461 msg.text match { |
456 case Protocol.Removed(removed) => |
462 case Protocol.Removed(removed) => |
457 try { |
463 try { |
458 global_state.change(_.removed_versions(removed)) |
464 global_state.change(_.removed_versions(removed)) |
459 manager.send(Session.Change_Flush) |
465 manager.send(Session.Change_Flush) |
460 } |
466 } |
461 catch { case _: Document.State.Fail => bad_output() } |
467 catch { case _: Document.State.Fail => bad_output(output) } |
462 case _ => bad_output() |
468 case _ => bad_output(output) |
463 } |
469 } |
464 |
470 |
465 case Markup.ML_Statistics(props) => |
471 case Markup.ML_Statistics(props) => |
466 statistics.post(Session.Statistics(props)) |
472 statistics.post(Session.Statistics(props)) |
467 |
473 |
468 case Markup.Task_Statistics(props) => |
474 case Markup.Task_Statistics(props) => |
469 // FIXME |
475 // FIXME |
470 |
476 |
471 case _ => bad_output() |
477 case _ => bad_output(output) |
472 } |
478 } |
473 } |
479 } |
474 case _ => |
480 case _ => |
475 output.properties match { |
481 output.properties match { |
476 case Position.Id(state_id) => |
482 case Position.Id(state_id) => |
553 prover.get.dialog_result(serial, result) |
559 prover.get.dialog_result(serial, result) |
554 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
560 handle_output(new Prover.Output(Protocol.Dialog_Result(id, serial, result))) |
555 |
561 |
556 case Protocol_Command(name, args) if prover.defined => |
562 case Protocol_Command(name, args) if prover.defined => |
557 prover.get.protocol_command(name, args:_*) |
563 prover.get.protocol_command(name, args:_*) |
|
564 |
|
565 case Add_Export(args, bytes, output) => |
|
566 val id = Value.Long.parse(args.id.get) |
|
567 val entry = (args.serial, Export.make_entry("", args, bytes)) |
|
568 change_command(_.add_export(id, entry), output) |
558 |
569 |
559 case change: Session.Change if prover.defined => |
570 case change: Session.Change if prover.defined => |
560 val state = global_state.value |
571 val state = global_state.value |
561 if (!state.removing_versions && state.is_assigned(change.previous)) |
572 if (!state.removing_versions && state.is_assigned(change.previous)) |
562 handle_change(change) |
573 handle_change(change) |