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 class Commands_Changed(set: Set[Command])
26 class Session(system: Isabelle_System)
28 /* real time parameters */ // FIXME properties or settings (!?)
30 // user input (e.g. text edits, cursor movement)
33 // prover output (markup, common messages)
34 val output_delay = 100
37 val update_delay = 500
40 /* pervasive event buses */
42 val global_settings = new Event_Bus[Session.Global_Settings.type]
43 val raw_protocol = new Event_Bus[Isabelle_Process.Result]
44 val raw_output = 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]
51 private var id_count: Document.ID = 0
52 def new_id(): Document.ID = synchronized {
53 require(id_count > java.lang.Long.MIN_VALUE)
62 @volatile private var syntax = new Outer_Syntax(system.symbols)
63 def current_syntax: Outer_Syntax = syntax
65 @volatile private var global_state = Document.State.init
66 private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
67 def current_state(): Document.State = global_state
69 private case class Started(timeout: Int, args: List[String])
70 private case object Stop
72 private lazy val session_actor = actor {
74 var prover: Isabelle_Process with Isar_Document = null
77 /* document changes */
79 def handle_change(change: Document.Change)
82 require(change.is_finished)
84 val previous = change.previous.join
85 val (node_edits, current) = change.result.join
87 var former_assignment = current_state().the_assignment(previous).join
89 (name, Some(cmd_edits)) <- node_edits
90 (prev, None) <- cmd_edits
91 removed <- previous.nodes(name).commands.get_after(prev)
92 } former_assignment -= removed
96 case (name, None) => (name, None)
97 case (name, Some(cmd_edits)) =>
101 val id1 = c1.map(_.id)
105 case Some(command) =>
106 if (current_state().lookup_command(command.id).isEmpty) {
107 change_state(_.define_command(command))
108 prover.define_command(command.id, system.symbols.encode(command.source))
116 change_state(_.define_version(current, former_assignment))
117 prover.edit_version(previous.id, current.id, id_edits)
124 def bad_result(result: Isabelle_Process.Result)
126 System.err.println("Ignoring prover result: " + result.message.toString)
129 def handle_result(result: Isabelle_Process.Result)
132 raw_protocol.event(result)
134 Position.get_id(result.properties) match {
135 case Some(state_id) =>
137 val (st, state) = global_state.accumulate(state_id, result.message)
139 indicate_command_change(st.command)
141 catch { case _: Document.State.Fail => bad_result(result) }
143 if (result.is_status) {
145 case List(Isar_Document.Assign(id, edits)) =>
146 try { change_state(_.assign(id, edits)) }
147 catch { case _: Document.State.Fail => bad_result(result) }
148 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
149 case List(Keyword.Keyword_Decl(name)) => syntax += name
150 case _ => if (!result.is_ready) bad_result(result)
153 else if (result.kind == Markup.EXIT) prover = null
154 else if (result.is_raw) raw_output.event(result)
155 else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?)
163 def startup_error(): String =
165 val buf = new StringBuilder
168 case result: Isabelle_Process.Result =>
170 for (text <- XML.content(result.message))
174 case TIMEOUT => false
179 def prover_startup(timeout: Int): Option[String] =
181 receiveWithin(timeout) {
182 case result: Isabelle_Process.Result
183 if result.kind == Markup.INIT =>
185 case result: Isabelle_Process.Result =>
186 handle_result(result); !result.is_ready
190 case result: Isabelle_Process.Result
191 if result.kind == Markup.EXIT =>
192 Some(startup_error())
194 case TIMEOUT => // FIXME clarify
195 prover.kill; Some(startup_error())
204 case Started(timeout, args) =>
205 if (prover == null) {
206 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
208 val opt_err = prover_startup(timeout)
209 if (opt_err.isDefined) prover = null
214 case Stop => // FIXME clarify; synchronous
215 if (prover != null) {
220 case change: Document.Change if prover != null =>
221 handle_change(change)
223 case result: Isabelle_Process.Result =>
224 handle_result(result)
226 case TIMEOUT => // FIXME clarify!
228 case bad if prover != null =>
229 System.err.println("session_actor: ignoring bad message " + bad)
236 /** buffered command changes (delay_first discipline) **/
238 private lazy val command_change_buffer = actor
241 import scala.compat.Platform.currentTime
243 var changed: Set[Command] = Set()
244 var flush_time: Option[Long] = None
246 def flush_timeout: Long =
249 case Some(time) => (time - currentTime) max 0
254 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
261 val now = currentTime
263 case None => flush_time = Some(now + output_delay)
264 case Some(time) => if (now >= time) flush()
269 reactWithin(flush_timeout) {
270 case command: Command => changed += command; invoke()
271 case TIMEOUT => flush()
272 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
278 def indicate_command_change(command: Command)
280 command_change_buffer ! command
285 /** editor history **/
287 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
289 private val editor_history = new Actor
291 @volatile private var history = Document.History.init
293 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
294 history.snapshot(name, pending_edits, current_state())
300 case Edit_Version(edits) =>
301 val prev = history.tip.current
303 isabelle.Future.fork {
304 val previous = prev.join
305 val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
306 Thy_Syntax.text_edits(Session.this, previous, edits)
308 val change = new Document.Change(prev, edits, result)
310 change.current.map(_ => session_actor ! change)
313 case bad => System.err.println("editor_model: ignoring bad message " + bad)
324 def started(timeout: Int, args: List[String]): Option[String] =
325 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
327 def stop() { session_actor ! Stop }
329 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
330 editor_history.snapshot(name, pending_edits)
332 def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }