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())
202 val xml_cache = new XML.Cache(131071)
206 case Started(timeout, args) =>
207 if (prover == null) {
208 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
210 val opt_err = prover_startup(timeout)
211 if (opt_err.isDefined) prover = null
216 case Stop => // FIXME clarify; synchronous
217 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.cache(xml_cache))
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 lazy 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 private val editor_history = new Actor
293 @volatile private var history = List(Document.Change.init)
295 def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
297 val state_snapshot = current_state()
298 val history_snapshot = history
300 val found_stable = history_snapshot.find(change =>
301 change.is_finished && state_snapshot.is_assigned(change.current.join))
302 require(found_stable.isDefined)
303 val stable = found_stable.get
304 val latest = history_snapshot.head
307 (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
308 (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
309 lazy val reverse_edits = edits.reverse
311 new Document.Snapshot {
312 val version = stable.current.join
313 val node = version.nodes(name)
314 val is_outdated = !(pending_edits.isEmpty && latest == stable)
315 def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
316 def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
317 def lookup_command(id: Document.Command_ID): Option[Command] =
318 state_snapshot.lookup_command(id)
319 def state(command: Command): Command.State =
320 try { state_snapshot.command_state(version, command) }
321 catch { case _: Document.State.Fail => command.empty_state }
329 case Edit_Version(edits) =>
330 val history_snapshot = history
331 require(!history_snapshot.isEmpty)
333 val prev = history_snapshot.head.current
335 isabelle.Future.fork {
336 val previous = prev.join
337 val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
338 Thy_Syntax.text_edits(Session.this, previous, edits)
340 val new_change = new Document.Change(prev, edits, result)
341 history ::= new_change
342 new_change.current.map(_ => session_actor ! new_change)
345 case bad => System.err.println("editor_model: ignoring bad message " + bad)
356 def started(timeout: Int, args: List[String]): Option[String] =
357 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
359 def stop() { session_actor ! Stop }
361 def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
362 editor_history.snapshot(name, pending_edits)
364 def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }