equal
deleted
inserted
replaced
22 case object Assignment |
22 case object Assignment |
23 case class Commands_Changed(set: Set[Command]) |
23 case class Commands_Changed(set: Set[Command]) |
24 |
24 |
25 sealed abstract class Phase |
25 sealed abstract class Phase |
26 case object Inactive extends Phase |
26 case object Inactive extends Phase |
27 case object Startup extends Phase |
|
28 case object Exit extends Phase |
27 case object Exit extends Phase |
29 case object Ready extends Phase |
28 case object Ready extends Phase |
30 case object Shutdown extends Phase |
29 case object Shutdown extends Phase |
31 case object Terminated extends Phase |
|
32 } |
30 } |
33 |
31 |
34 |
32 |
35 class Session(system: Isabelle_System) |
33 class Session(system: Isabelle_System) |
36 { |
34 { |
124 @volatile private var reverse_syslog = List[XML.Elem]() |
122 @volatile private var reverse_syslog = List[XML.Elem]() |
125 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n") |
123 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n") |
126 |
124 |
127 @volatile private var _phase: Session.Phase = Session.Inactive |
125 @volatile private var _phase: Session.Phase = Session.Inactive |
128 def phase = _phase |
126 def phase = _phase |
129 def phase_=(new_phase: Session.Phase) |
127 private def phase_=(new_phase: Session.Phase) |
130 { |
128 { |
131 val old_phase = _phase |
129 val old_phase = _phase |
132 _phase = new_phase |
130 _phase = new_phase |
133 phase_changed.event(old_phase, new_phase) |
131 phase_changed.event(old_phase, new_phase) |
134 } |
132 } |
209 catch { case _: Document.State.Fail => bad_result(result) } |
207 catch { case _: Document.State.Fail => bad_result(result) } |
210 case _ => |
208 case _ => |
211 if (result.is_syslog) { |
209 if (result.is_syslog) { |
212 reverse_syslog ::= result.message |
210 reverse_syslog ::= result.message |
213 if (result.is_ready) phase = Session.Ready |
211 if (result.is_ready) phase = Session.Ready |
214 else if (result.is_exit) phase = Session.Exit |
212 else if (result.is_exit) { |
|
213 phase = Session.Exit |
|
214 phase = Session.Inactive |
|
215 } |
215 } |
216 } |
216 else if (result.is_stdout) { } |
217 else if (result.is_stdout) { } |
217 else if (result.is_status) { |
218 else if (result.is_status) { |
218 result.body match { |
219 result.body match { |
219 case List(Isar_Document.Assign(id, edits)) => |
220 case List(Isar_Document.Assign(id, edits)) => |
257 case change: Document.Change if prover != null => handle_change(change) |
258 case change: Document.Change if prover != null => handle_change(change) |
258 |
259 |
259 case result: Isabelle_Process.Result => handle_result(result) |
260 case result: Isabelle_Process.Result => handle_result(result) |
260 |
261 |
261 case Start(timeout, args) if prover == null => |
262 case Start(timeout, args) if prover == null => |
262 phase = Session.Startup |
|
263 prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document |
263 prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document |
264 |
264 |
265 case Stop if phase == Session.Ready => |
265 case Stop if phase == Session.Ready => |
266 global_state.change(_ => Document.State.init) // FIXME event bus!? |
266 global_state.change(_ => Document.State.init) // FIXME event bus!? |
267 phase = Session.Shutdown |
267 phase = Session.Shutdown |
268 prover.terminate |
268 prover.terminate |
269 phase = Session.Terminated |
269 phase = Session.Inactive |
270 finished = true |
270 finished = true |
271 reply(()) |
271 reply(()) |
272 |
272 |
273 case bad if prover != null => |
273 case bad if prover != null => |
274 System.err.println("session_actor: ignoring bad message " + bad) |
274 System.err.println("session_actor: ignoring bad message " + bad) |