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_results = 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 create_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 old_doc = change.prev.join
85 val (node_edits, doc) = change.result.join
87 var former_assignment = current_state().the_assignment(old_doc).join
89 (name, Some(cmd_edits)) <- node_edits
90 (prev, None) <- cmd_edits
91 removed <- old_doc.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_document(doc, former_assignment))
117 prover.edit_document(old_doc.id, doc.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_results.event(result)
134 Position.get_id(result.properties) match {
135 case Some(target_id) =>
137 val (st, state) = global_state.accumulate(target_id, result.message)
139 indicate_command_change(st.command) // FIXME forward Command.State (!?)
142 case _: Document.State.Fail =>
143 if (result.is_status) {
145 case List(Isar_Document.Assign(edits)) =>
146 try { change_state(_.assign(target_id, edits)) }
147 catch { case _: Document.State.Fail => bad_result(result) }
148 case _ => bad_result(result)
151 else bad_result(result)
154 if (result.is_status) {
156 // keyword declarations // FIXME always global!?
157 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
158 case List(Keyword.Keyword_Decl(name)) => syntax += name
159 case _ => if (!result.is_ready) bad_result(result)
162 else if (result.kind == Markup.EXIT) prover = null
163 else if (result.is_raw) raw_output.event(result)
164 else if (!result.is_system) bad_result(result) // FIXME syslog for system messages (!?)
172 def startup_error(): String =
174 val buf = new StringBuilder
177 case result: Isabelle_Process.Result =>
179 for (text <- XML.content(result.message))
183 case TIMEOUT => false
188 def prover_startup(timeout: Int): Option[String] =
190 receiveWithin(timeout) {
191 case result: Isabelle_Process.Result
192 if result.kind == Markup.INIT =>
194 case result: Isabelle_Process.Result =>
195 handle_result(result); !result.is_ready
199 case result: Isabelle_Process.Result
200 if result.kind == Markup.EXIT =>
201 Some(startup_error())
203 case TIMEOUT => // FIXME clarify
204 prover.kill; Some(startup_error())
211 val xml_cache = new XML.Cache(131071)
215 case Started(timeout, args) =>
216 if (prover == null) {
217 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
219 val opt_err = prover_startup(timeout)
220 if (opt_err.isDefined) prover = null
225 case Stop => // FIXME clarify; synchronous
226 if (prover != null) {
231 case change: Document.Change if prover != null =>
232 handle_change(change)
234 case result: Isabelle_Process.Result =>
235 handle_result(result.cache(xml_cache))
237 case TIMEOUT => // FIXME clarify!
239 case bad if prover != null =>
240 System.err.println("session_actor: ignoring bad message " + bad)
247 /** buffered command changes (delay_first discipline) **/
249 private lazy val command_change_buffer = actor
252 import scala.compat.Platform.currentTime
254 var changed: Set[Command] = Set()
255 var flush_time: Option[Long] = None
257 def flush_timeout: Long =
260 case Some(time) => (time - currentTime) max 0
265 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
272 val now = currentTime
274 case None => flush_time = Some(now + output_delay)
275 case Some(time) => if (now >= time) flush()
280 reactWithin(flush_timeout) {
281 case command: Command => changed += command; invoke()
282 case TIMEOUT => flush()
283 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
289 def indicate_command_change(command: Command)
291 command_change_buffer ! command
296 /** editor history **/
298 private case class Edit_Document(edits: List[Document.Node_Text_Edit])
300 private val editor_history = new Actor
302 @volatile private var history = List(Document.Change.init)
304 def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
306 val state_snapshot = current_state()
307 val history_snapshot = history
309 val found_stable = history_snapshot.find(change =>
310 change.is_finished && state_snapshot.is_assigned(change.document.join))
311 require(found_stable.isDefined)
312 val stable = found_stable.get
313 val latest = history_snapshot.head
316 (pending_edits /: history_snapshot.takeWhile(_ != stable))((edits, change) =>
317 (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
318 lazy val reverse_edits = edits.reverse
320 new Document.Snapshot {
321 val document = stable.document.join
322 val node = document.nodes(name)
323 val is_outdated = !(pending_edits.isEmpty && latest == stable)
324 def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
325 def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
326 def lookup_command(id: Document.Command_ID): Option[Command] =
327 state_snapshot.lookup_command(id)
328 def state(command: Command): Command.State =
329 state_snapshot.command_state(document, command)
337 case Edit_Document(edits) =>
338 val history_snapshot = history
339 require(!history_snapshot.isEmpty)
341 val prev = history_snapshot.head.document
342 val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
343 isabelle.Future.fork {
344 val old_doc = prev.join
345 val former_assignment = current_state().the_assignment(old_doc).join // FIXME async!?
346 Thy_Syntax.text_edits(Session.this, old_doc, edits)
348 val new_change = new Document.Change(prev, edits, result)
349 history ::= new_change
350 new_change.document.map(_ => session_actor ! new_change)
353 case bad => System.err.println("editor_model: ignoring bad message " + bad)
364 def started(timeout: Int, args: List[String]): Option[String] =
365 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
367 def stop() { session_actor ! Stop }
369 def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
370 editor_history.snapshot(name, pending_edits)
372 def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }