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 val session_actor = Simple_Thread.actor("session_actor", daemon = true)
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 result.properties match {
135 case Position.Id(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())
205 case Started(timeout, args) =>
206 if (prover == null) {
207 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
209 val opt_err = prover_startup(timeout)
210 if (opt_err.isDefined) prover = null
215 case Stop => // FIXME synchronous!?
216 if (prover != null) {
222 case change: Document.Change if prover != null =>
223 handle_change(change)
225 case result: Isabelle_Process.Result =>
226 handle_result(result)
228 case TIMEOUT => // FIXME clarify!
230 case bad if prover != null =>
231 System.err.println("session_actor: ignoring bad message " + bad)
238 /** buffered command changes (delay_first discipline) **/
240 private val command_change_buffer = actor
243 import scala.compat.Platform.currentTime
245 var changed: Set[Command] = Set()
246 var flush_time: Option[Long] = None
248 def flush_timeout: Long =
251 case Some(time) => (time - currentTime) max 0
256 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
263 val now = currentTime
265 case None => flush_time = Some(now + output_delay)
266 case Some(time) => if (now >= time) flush()
271 reactWithin(flush_timeout) {
272 case command: Command => changed += command; invoke()
273 case TIMEOUT => flush()
274 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
280 def indicate_command_change(command: Command)
282 command_change_buffer ! command
287 /** editor history **/
289 private case class Edit_Version(edits: List[Document.Node_Text_Edit])
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())
296 private val editor_history = actor
300 case Edit_Version(edits) =>
301 val prev = history.tip.current
303 // FIXME potential denial-of-service concerning worker pool (!?!?)
304 isabelle.Future.fork {
305 val previous = prev.join
306 val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
307 Thy_Syntax.text_edits(Session.this, previous, edits)
309 val change = new Document.Change(prev, edits, result)
311 change.current.map(_ => session_actor ! change)
314 case bad => System.err.println("editor_model: ignoring bad message " + bad)
323 def started(timeout: Int, args: List[String]): Option[String] =
324 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
326 def stop() { session_actor ! Stop }
328 def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }