69 |
69 |
70 sealed abstract class Phase |
70 sealed abstract class Phase |
71 { |
71 { |
72 def print: String = |
72 def print: String = |
73 this match { |
73 this match { |
74 case Terminated(rc) => if (rc == 0) "finished" else "failed" |
74 case Terminated(result) => if (result.ok) "finished" else "failed" |
75 case _ => Word.lowercase(this.toString) |
75 case _ => Word.lowercase(this.toString) |
76 } |
76 } |
77 } |
77 } |
78 case object Inactive extends Phase // stable |
78 case object Inactive extends Phase // stable |
79 case object Startup extends Phase // transient |
79 case object Startup extends Phase // transient |
80 case object Ready extends Phase // metastable |
80 case object Ready extends Phase // metastable |
81 case object Shutdown extends Phase // transient |
81 case object Shutdown extends Phase // transient |
82 case class Terminated(rc: Int) extends Phase // stable |
82 case class Terminated(result: Process_Result) extends Phase // stable |
83 //}}} |
83 //}}} |
84 |
84 |
85 |
85 |
86 /* syslog */ |
86 /* syslog */ |
87 |
87 |
444 case _ if output.is_init => |
444 case _ if output.is_init => |
445 prover.get.options(session_options) |
445 prover.get.options(session_options) |
446 phase = Session.Ready |
446 phase = Session.Ready |
447 debugger.ready() |
447 debugger.ready() |
448 |
448 |
449 case Markup.Return_Code(rc) if output.is_exit => |
449 case Markup.Process_Result(result) if output.is_exit => |
450 phase = Session.Terminated(rc) |
450 phase = Session.Terminated(result) |
451 prover.reset |
451 prover.reset |
452 |
452 |
453 case _ => |
453 case _ => |
454 raw_output_messages.post(output) |
454 raw_output_messages.post(output) |
455 } |
455 } |
559 val was_ready = |
559 val was_ready = |
560 _phase.guarded_access(phase => |
560 _phase.guarded_access(phase => |
561 phase match { |
561 phase match { |
562 case Session.Startup | Session.Shutdown => None |
562 case Session.Startup | Session.Shutdown => None |
563 case Session.Terminated(_) => Some((false, phase)) |
563 case Session.Terminated(_) => Some((false, phase)) |
564 case Session.Inactive => Some((false, post_phase(Session.Terminated(0)))) |
564 case Session.Inactive => Some((false, post_phase(Session.Terminated(Process_Result(0))))) |
565 case Session.Ready => Some((true, post_phase(Session.Shutdown))) |
565 case Session.Ready => Some((true, post_phase(Session.Shutdown))) |
566 }) |
566 }) |
567 if (was_ready) manager.send(Stop) |
567 if (was_ready) manager.send(Stop) |
568 } |
568 } |
569 |
569 |
570 def stop(): Int = |
570 def stop(): Process_Result = |
571 { |
571 { |
572 send_stop() |
572 send_stop() |
573 prover.await_reset() |
573 prover.await_reset() |
574 |
574 |
575 change_parser.shutdown() |
575 change_parser.shutdown() |
576 change_buffer.shutdown() |
576 change_buffer.shutdown() |
577 manager.shutdown() |
577 manager.shutdown() |
578 dispatcher.shutdown() |
578 dispatcher.shutdown() |
579 |
579 |
580 phase match { |
580 phase match { |
581 case Session.Terminated(rc) => rc |
581 case Session.Terminated(result) => result |
582 case phase => error("Bad session phase after shutdown: " + quote(phase.print)) |
582 case phase => error("Bad session phase after shutdown: " + quote(phase.print)) |
583 } |
583 } |
584 } |
584 } |
585 |
585 |
586 def protocol_command(name: String, args: String*) |
586 def protocol_command(name: String, args: String*) |