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])
27 class Session(system: Isabelle_System)
29 /* real time parameters */ // FIXME properties or settings (!?)
31 // user input (e.g. text edits, cursor movement)
34 // prover output (markup, common messages)
35 val output_delay = 100
38 val update_delay = 500
41 /* pervasive event buses */
43 val global_settings = new Event_Bus[Session.Global_Settings.type]
44 val raw_messages = new Event_Bus[Isabelle_Process.Result]
45 val commands_changed = new Event_Bus[Session.Commands_Changed]
46 val perspective = new Event_Bus[Session.Perspective.type]
47 val assignments = new Event_Bus[Session.Assignment.type]
52 private var id_count: Document.ID = 0
53 def new_id(): Document.ID = synchronized {
54 require(id_count > java.lang.Long.MIN_VALUE)
61 /** buffered command changes (delay_first discipline) **/
63 private case object Stop
65 private val (_, command_change_buffer) =
66 Simple_Thread.actor("command_change_buffer", daemon = true)
69 import scala.compat.Platform.currentTime
71 var changed: Set[Command] = Set()
72 var flush_time: Option[Long] = None
74 def flush_timeout: Long =
77 case Some(time) => (time - currentTime) max 0
82 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
91 case None => flush_time = Some(now + output_delay)
92 case Some(time) => if (now >= time) flush()
98 receiveWithin(flush_timeout) {
99 case command: Command => changed += command; invoke()
100 case TIMEOUT => flush()
101 case Stop => finished = true
102 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
110 /** main protocol actor **/
112 @volatile private var syntax = new Outer_Syntax(system.symbols)
113 def current_syntax(): Outer_Syntax = syntax
115 private val global_state = new Volatile(Document.State.init)
116 def current_state(): Document.State = global_state.peek()
118 private case object Interrupt_Prover
119 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
120 private case class Started(timeout: Int, args: List[String])
122 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
124 var prover: Isabelle_Process with Isar_Document = null
127 /* document changes */
129 def handle_change(change: Document.Change)
132 val previous = change.previous.get_finished
133 val (node_edits, current) = change.result.get_finished
135 var former_assignment = global_state.peek().the_assignment(previous).get_finished
137 (name, Some(cmd_edits)) <- node_edits
138 (prev, None) <- cmd_edits
139 removed <- previous.nodes(name).commands.get_after(prev)
140 } former_assignment -= removed
144 case (name, None) => (name, None)
145 case (name, Some(cmd_edits)) =>
149 val id1 = c1.map(_.id)
153 case Some(command) =>
154 if (global_state.peek().lookup_command(command.id).isEmpty) {
155 global_state.change(_.define_command(command))
156 prover.define_command(command.id, system.symbols.encode(command.source))
164 global_state.change(_.define_version(current, former_assignment))
165 prover.edit_version(previous.id, current.id, id_edits)
172 def bad_result(result: Isabelle_Process.Result)
174 System.err.println("Ignoring prover result: " + result.message.toString)
177 def handle_result(result: Isabelle_Process.Result)
180 raw_messages.event(result)
182 result.properties match {
183 case Position.Id(state_id) =>
185 val st = global_state.change_yield(_.accumulate(state_id, result.message))
186 command_change_buffer ! st.command
188 catch { case _: Document.State.Fail => bad_result(result) }
190 if (result.is_status) {
192 case List(Isar_Document.Assign(id, edits)) =>
194 val cmds: List[Command] = global_state.change_yield(_.assign(id, edits))
195 for (cmd <- cmds) command_change_buffer ! cmd
196 assignments.event(Session.Assignment)
198 catch { case _: Document.State.Fail => bad_result(result) }
199 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
200 case List(Keyword.Keyword_Decl(name)) => syntax += name
201 case _ => if (!result.is_ready) bad_result(result)
204 else if (result.is_exit) prover = null // FIXME ??
205 else if (!(result.is_init || result.is_exit || result.is_system || result.is_stdout))
214 def startup_error(): String =
216 val buf = new StringBuilder
219 case result: Isabelle_Process.Result =>
220 if (result.is_system) {
221 for (text <- XML.content(result.message))
225 case TIMEOUT => false
230 def prover_startup(timeout: Int): Option[String] =
232 receiveWithin(timeout) {
233 case result: Isabelle_Process.Result if result.is_init =>
234 handle_result(result)
236 case result: Isabelle_Process.Result =>
237 handle_result(result); !result.is_ready
241 case result: Isabelle_Process.Result if result.is_exit =>
242 handle_result(result)
243 Some(startup_error())
245 case TIMEOUT => // FIXME clarify
246 prover.terminate; Some(startup_error())
251 /* main loop */ // FIXME proper shutdown
256 case Interrupt_Prover =>
257 if (prover != null) prover.interrupt
259 case Edit_Version(edits) =>
260 val previous = global_state.peek().history.tip.current
261 val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
262 val change = global_state.change_yield(_.extend_history(previous, edits, result))
264 val this_actor = self
265 change.current.map(_ => {
266 assignments.await { global_state.peek().is_assigned(previous.get_finished) }
267 this_actor ! change })
271 case change: Document.Change if prover != null =>
272 handle_change(change)
274 case result: Isabelle_Process.Result =>
275 handle_result(result)
277 case Started(timeout, args) =>
278 if (prover == null) {
279 prover = new Isabelle_Process(system, timeout, self, args:_*) with Isar_Document
281 val opt_err = prover_startup(timeout + 500)
282 if (opt_err.isDefined) prover = null
287 case Stop => // FIXME synchronous!?
288 if (prover != null) {
289 global_state.change(_ => Document.State.init)
294 case TIMEOUT => // FIXME clarify
296 case bad if prover != null =>
297 System.err.println("session_actor: ignoring bad message " + bad)
306 def started(timeout: Int, args: List[String]): Option[String] =
307 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
309 def stop() { command_change_buffer ! Stop; session_actor ! Stop }
311 def interrupt() { session_actor ! Interrupt_Prover }
313 def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
315 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
316 global_state.peek().snapshot(name, pending_edits)