1 /* Title: Pure/System/session.scala
3 Options: :folding=explicit:collapseFolds=1:
5 Isabelle session, potentially with running prover.
11 import scala.actors.TIMEOUT
12 import scala.actors.Actor
13 import scala.actors.Actor._
20 case object Global_Settings
21 case object Perspective
22 case object Assignment
23 case class Commands_Changed(set: Set[Command])
25 sealed abstract class Phase
26 case object Inactive extends Phase
27 case object Startup extends Phase
28 case object Ready extends Phase
29 case object Shutdown extends Phase
33 class Session(system: Isabelle_System)
35 /* real time parameters */ // FIXME properties or settings (!?)
37 // user input (e.g. text edits, cursor movement)
40 // prover output (markup, common messages)
41 val output_delay = 100
44 val update_delay = 500
47 /* pervasive event buses */
49 val phase_changed = new Event_Bus[(Session.Phase, Session.Phase)]
50 val global_settings = new Event_Bus[Session.Global_Settings.type]
51 val raw_messages = new Event_Bus[Isabelle_Process.Result]
52 val commands_changed = new Event_Bus[Session.Commands_Changed]
53 val perspective = new Event_Bus[Session.Perspective.type]
54 val assignments = new Event_Bus[Session.Assignment.type]
59 private var id_count: Document.ID = 0
60 def new_id(): Document.ID = synchronized {
61 require(id_count > java.lang.Long.MIN_VALUE)
68 /** buffered command changes (delay_first discipline) **/
70 private case object Stop
72 private val (_, command_change_buffer) =
73 Simple_Thread.actor("command_change_buffer", daemon = true)
76 import scala.compat.Platform.currentTime
78 var changed: Set[Command] = Set()
79 var flush_time: Option[Long] = None
81 def flush_timeout: Long =
84 case Some(time) => (time - currentTime) max 0
89 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
98 case None => flush_time = Some(now + output_delay)
99 case Some(time) => if (now >= time) flush()
105 receiveWithin(flush_timeout) {
106 case command: Command => changed += command; invoke()
107 case TIMEOUT => flush()
108 case Stop => finished = true; reply(())
109 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
117 /** main protocol actor **/
119 @volatile private var syntax = new Outer_Syntax(system.symbols)
120 def current_syntax(): Outer_Syntax = syntax
122 @volatile private var reverse_syslog = List[XML.Elem]()
123 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
125 @volatile private var _phase: Session.Phase = Session.Inactive
127 private def phase_=(new_phase: Session.Phase)
129 val old_phase = _phase
131 phase_changed.event(old_phase, new_phase)
134 private val global_state = new Volatile(Document.State.init)
135 def current_state(): Document.State = global_state.peek()
137 private case object Interrupt_Prover
138 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
139 private case class Start(timeout: Int, args: List[String])
141 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
143 var prover: Isabelle_Process with Isar_Document = null
146 /* document changes */
148 def handle_change(change: Document.Change)
151 val previous = change.previous.get_finished
152 val (node_edits, version) = change.result.get_finished
154 var former_assignment = global_state.peek().the_assignment(previous).get_finished
156 (name, Some(cmd_edits)) <- node_edits
157 (prev, None) <- cmd_edits
158 removed <- previous.nodes(name).commands.get_after(prev)
159 } former_assignment -= removed
163 case (name, None) => (name, None)
164 case (name, Some(cmd_edits)) =>
168 val id1 = c1.map(_.id)
172 case Some(command) =>
173 if (global_state.peek().lookup_command(command.id).isEmpty) {
174 global_state.change(_.define_command(command))
175 prover.define_command(command.id, system.symbols.encode(command.source))
183 global_state.change(_.define_version(version, former_assignment))
184 prover.edit_version(previous.id, version.id, id_edits)
191 def bad_result(result: Isabelle_Process.Result)
193 System.err.println("Ignoring prover result: " + result.message.toString)
196 def handle_result(result: Isabelle_Process.Result)
199 raw_messages.event(result)
201 result.properties match {
202 case Position.Id(state_id) =>
204 val st = global_state.change_yield(_.accumulate(state_id, result.message))
205 command_change_buffer ! st.command
207 catch { case _: Document.State.Fail => bad_result(result) }
209 if (result.is_syslog) {
210 reverse_syslog ::= result.message
211 if (result.is_ready) phase = Session.Ready
212 else if (result.is_exit) phase = Session.Inactive
214 else if (result.is_stdout) { }
215 else if (result.is_status) {
217 case List(Isar_Document.Assign(id, edits)) =>
219 val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
220 for (cmd <- cmds) command_change_buffer ! cmd
221 assignments.event(Session.Assignment)
223 catch { case _: Document.State.Fail => bad_result(result) }
224 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
225 case List(Keyword.Keyword_Decl(name)) => syntax += name
226 case _ => bad_result(result)
229 else bad_result(result)
240 case Interrupt_Prover =>
241 if (prover != null) prover.interrupt
243 case Edit_Version(edits) if prover != null =>
244 val previous = global_state.peek().history.tip.version
245 val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
246 val change = global_state.change_yield(_.extend_history(previous, edits, result))
248 val this_actor = self
249 change.version.map(_ => {
250 assignments.await { global_state.peek().is_assigned(previous.get_finished) }
251 this_actor ! change })
255 case change: Document.Change if prover != null => handle_change(change)
257 case result: Isabelle_Process.Result => handle_result(result)
259 case Start(timeout, args) if prover == null =>
260 phase = Session.Startup
261 prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
263 case Stop if phase == Session.Ready =>
264 global_state.change(_ => Document.State.init) // FIXME event bus!?
265 phase = Session.Shutdown
267 phase = Session.Inactive
271 case bad if prover != null =>
272 System.err.println("session_actor: ignoring bad message " + bad)
281 def start(timeout: Int, args: List[String]) { session_actor ! Start(timeout, args) }
283 def stop() { command_change_buffer !? Stop; session_actor !? Stop }
285 def interrupt() { session_actor ! Interrupt_Prover }
287 def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
289 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
290 global_state.peek().snapshot(name, pending_edits)