clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;
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 /* managed entities */
31 def consume(message: XML.Tree, forward: Command => Unit): Unit
36 class Session(system: Isabelle_System)
38 /* real time parameters */ // FIXME properties or settings (!?)
40 // user input (e.g. text edits, cursor movement)
43 // prover output (markup, common messages)
44 val output_delay = 100
47 val update_delay = 500
50 /* pervasive event buses */
52 val global_settings = new Event_Bus[Session.Global_Settings.type]
53 val raw_results = new Event_Bus[Isabelle_Process.Result]
54 val raw_output = new Event_Bus[Isabelle_Process.Result]
55 val commands_changed = new Event_Bus[Session.Commands_Changed]
56 val perspective = new Event_Bus[Session.Perspective.type]
61 private var id_count: Document.ID = 0
62 def create_id(): Document.ID = synchronized {
63 require(id_count > java.lang.Long.MIN_VALUE)
72 @volatile private var syntax = new Outer_Syntax(system.symbols)
73 def current_syntax: Outer_Syntax = syntax
75 @volatile private var entities = Map[Document.ID, Session.Entity]()
76 def lookup_entity(id: Document.ID): Option[Session.Entity] = entities.get(id)
77 def lookup_command(id: Document.ID): Option[Command] =
78 lookup_entity(id) match {
79 case Some(cmd: Command) => Some(cmd)
83 private case class Started(timeout: Int, args: List[String])
84 private case object Stop
86 private lazy val session_actor = actor {
88 var prover: Isabelle_Process with Isar_Document = null
90 def register(entity: Session.Entity) { entities += (entity.id -> entity) }
92 var documents = Map[Document.Version_ID, Document]()
93 def register_document(doc: Document) { documents += (doc.id -> doc) }
94 register_document(Document.init)
97 /* document changes */
99 def handle_change(change: Document.Change)
102 require(change.parent.isDefined)
104 val (node_edits, doc) = change.result.join
107 case (name, None) => (name, None)
108 case (name, Some(cmd_edits)) =>
112 val id1 = c1.map(_.id)
116 case Some(command) =>
117 if (!lookup_command(command.id).isDefined) {
119 prover.define_command(command.id, system.symbols.encode(command.source))
127 register_document(doc)
128 prover.edit_document(change.parent.get.id, doc.id, id_edits)
135 def bad_result(result: Isabelle_Process.Result)
137 System.err.println("Ignoring prover result: " + result.message.toString)
140 def handle_result(result: Isabelle_Process.Result)
143 raw_results.event(result)
145 val target_id: Option[Document.ID] = Position.get_id(result.properties)
146 val target: Option[Session.Entity] =
149 case Some(id) => lookup_entity(id)
151 if (target.isDefined) target.get.consume(result.message, indicate_command_change)
152 else if (result.is_status) {
153 // global status message
156 // execution assignment
157 case List(Isar_Document.Assign(edits)) if target_id.isDefined =>
158 documents.get(target_id.get) match {
162 Isar_Document.Edit(cmd_id, exec_id) <- edits
163 cmd <- lookup_command(cmd_id)
165 val st = cmd.assign_exec(exec_id) // FIXME session state
169 doc.assign_execs(execs) // FIXME session state
170 case None => bad_result(result)
173 // keyword declarations
174 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
175 case List(Keyword.Keyword_Decl(name)) => syntax += name
177 case _ => if (!result.is_ready) bad_result(result)
180 else if (result.kind == Markup.EXIT)
182 else if (result.is_raw)
183 raw_output.event(result)
184 else if (!result.is_system) // FIXME syslog (!?)
192 def startup_error(): String =
194 val buf = new StringBuilder
197 case result: Isabelle_Process.Result =>
199 for (text <- XML.content(result.message))
203 case TIMEOUT => false
208 def prover_startup(timeout: Int): Option[String] =
210 receiveWithin(timeout) {
211 case result: Isabelle_Process.Result
212 if result.kind == Markup.INIT =>
214 case result: Isabelle_Process.Result =>
215 handle_result(result); !result.is_ready
219 case result: Isabelle_Process.Result
220 if result.kind == Markup.EXIT =>
221 Some(startup_error())
223 case TIMEOUT => // FIXME clarify
224 prover.kill; Some(startup_error())
231 val xml_cache = new XML.Cache(131071)
235 case Started(timeout, args) =>
236 if (prover == null) {
237 prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
239 val opt_err = prover_startup(timeout)
240 if (opt_err.isDefined) prover = null
245 case Stop => // FIXME clarify; synchronous
246 if (prover != null) {
251 case change: Document.Change if prover != null =>
252 handle_change(change)
254 case result: Isabelle_Process.Result =>
255 handle_result(result.cache(xml_cache))
257 case TIMEOUT => // FIXME clarify!
259 case bad if prover != null =>
260 System.err.println("session_actor: ignoring bad message " + bad)
267 /** buffered command changes (delay_first discipline) **/
269 private lazy val command_change_buffer = actor
272 import scala.compat.Platform.currentTime
274 var changed: Set[Command] = Set()
275 var flush_time: Option[Long] = None
277 def flush_timeout: Long =
280 case Some(time) => (time - currentTime) max 0
285 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
292 val now = currentTime
294 case None => flush_time = Some(now + output_delay)
295 case Some(time) => if (now >= time) flush()
300 reactWithin(flush_timeout) {
301 case command: Command => changed += command; invoke()
302 case TIMEOUT => flush()
303 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
309 def indicate_command_change(command: Command)
311 command_change_buffer ! command
316 /** editor history **/
318 private case class Edit_Document(edits: List[Document.Node_Text_Edit])
320 private val editor_history = new Actor
322 @volatile private var history = Document.Change.init
323 def current_change(): Document.Change = history
329 case Edit_Document(edits) =>
330 val old_change = history
331 val new_id = create_id()
332 val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
333 isabelle.Future.fork {
334 val old_doc = old_change.join_document
335 old_doc.await_assignment
336 Document.text_edits(Session.this, old_doc, new_id, edits)
338 val new_change = new Document.Change(new_id, Some(old_change), edits, result)
340 new_change.result.map(_ => session_actor ! new_change)
343 case bad => System.err.println("editor_model: ignoring bad message " + bad)
354 def started(timeout: Int, args: List[String]): Option[String] =
355 (session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
357 def stop() { session_actor ! Stop }
359 def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
360 editor_history.current_change().snapshot(name, pending_edits)
362 def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }