1 /* Title: Pure/System/session.scala
3 Options: :folding=explicit:collapseFolds=1:
5 Main Isabelle/Scala session, potentially with running prover process.
11 import java.lang.System
12 import java.util.{Timer, TimerTask}
14 import scala.collection.mutable
15 import scala.actors.TIMEOUT
16 import scala.actors.Actor._
24 case object Global_Settings
25 case object Caret_Focus
26 case class Commands_Changed(nodes: Set[Document.Node.Name], commands: Set[Command])
28 sealed abstract class Phase
29 case object Inactive extends Phase
30 case object Startup extends Phase // transient
31 case object Failed extends Phase
32 case object Ready extends Phase
33 case object Shutdown extends Phase // transient
38 class Session(thy_load: Thy_Load = new Thy_Load)
40 /* real time parameters */ // FIXME properties or settings (!?)
42 val message_delay = Time.seconds(0.01) // prover messages
43 val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
44 val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
45 val update_delay = Time.seconds(0.5) // GUI layout updates
46 val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.)
47 val prune_delay = Time.seconds(60.0) // prune history -- delete old versions
48 val prune_size = 0 // size of retained history
51 /* pervasive event buses */
53 val global_settings = new Event_Bus[Session.Global_Settings.type]
54 val caret_focus = new Event_Bus[Session.Caret_Focus.type]
55 val commands_changed = new Event_Bus[Session.Commands_Changed]
56 val phase_changed = new Event_Bus[Session.Phase]
57 val syslog_messages = new Event_Bus[Isabelle_Process.Result]
58 val raw_output_messages = new Event_Bus[Isabelle_Process.Result]
59 val protocol_messages = new Event_Bus[Isabelle_Process.Message] // potential bottle-neck
63 /** buffered command changes (delay_first discipline) **/
66 private case object Stop
68 private val (_, commands_changed_buffer) =
69 Simple_Thread.actor("commands_changed_buffer", daemon = true)
74 case Stop => finished = true; reply(())
75 case changed: Session.Commands_Changed => commands_changed.event(changed)
76 case bad => System.err.println("commands_changed_buffer: ignoring bad message " + bad)
83 /** pipelined change parsing **/
86 private case class Text_Edits(
88 name: Document.Node.Name,
89 previous: Future[Document.Version],
90 text_edits: List[Document.Edit_Text],
91 version_result: Promise[Document.Version])
93 private val (_, change_parser) = Simple_Thread.actor("change_parser", daemon = true)
98 case Stop => finished = true; reply(())
100 case Text_Edits(syntax, name, previous, text_edits, version_result) =>
101 val prev = previous.get_finished
102 val (doc_edits, version) = Thy_Syntax.text_edits(syntax, prev, text_edits)
103 version_result.fulfill(version)
104 sender ! Change_Node(name, doc_edits, prev, version)
106 case bad => System.err.println("change_parser: ignoring bad message " + bad)
113 /** main protocol actor **/
117 @volatile var verbose: Boolean = false
119 @volatile private var syntax = new Outer_Syntax
120 def current_syntax(): Outer_Syntax = syntax
122 @volatile private var reverse_syslog = List[XML.Elem]()
123 def syslog(): String = cat_lines(reverse_syslog.reverse.map(msg => XML.content(msg).mkString))
125 @volatile private var _phase: Session.Phase = Session.Inactive
126 private def phase_=(new_phase: Session.Phase)
129 phase_changed.event(new_phase)
132 def is_ready: Boolean = phase == Session.Ready
134 private val global_state = Volatile(Document.State.init)
135 def current_state(): Document.State = global_state()
137 def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
138 pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
139 global_state().snapshot(name, pending_edits)
144 def header_edit(name: Document.Node.Name, header: Document.Node_Header): Document.Edit_Text =
146 def norm_import(s: String): String =
148 val thy_name = Thy_Header.base_name(s)
149 if (thy_load.is_loaded(thy_name)) thy_name
150 else thy_load.append(name.dir, Thy_Header.thy_path(Path.explode(s)))
152 def norm_use(s: String): String = thy_load.append(name.dir, Path.explode(s))
154 val header1: Document.Node_Header =
156 case Exn.Res(Thy_Header(thy_name, _, _))
157 if (thy_load.is_loaded(thy_name)) =>
158 Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
159 case _ => Document.Node.norm_header(norm_import, norm_use, header)
161 (name, Document.Node.Header(header1))
167 private case class Start(timeout: Time, args: List[String])
168 private case object Cancel_Execution
169 private case class Init_Node(name: Document.Node.Name,
170 header: Document.Node_Header, perspective: Text.Perspective, text: String)
171 private case class Edit_Node(name: Document.Node.Name,
172 header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
173 private case class Change_Node(
174 name: Document.Node.Name,
175 doc_edits: List[Document.Edit_Command],
176 previous: Document.Version,
177 version: Document.Version)
178 private case class Messages(msgs: List[Isabelle_Process.Message])
180 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
182 val this_actor = self
184 var prune_next = System.currentTimeMillis() + prune_delay.ms
187 /* buffered prover messages */
191 private var buffer = new mutable.ListBuffer[Isabelle_Process.Message]
193 def flush(): Unit = synchronized {
194 if (!buffer.isEmpty) {
195 val msgs = buffer.toList
196 this_actor ! Messages(msgs)
197 buffer = new mutable.ListBuffer[Isabelle_Process.Message]
200 def invoke(msg: Isabelle_Process.Message): Unit = synchronized {
203 case result: Isabelle_Process.Result if result.is_raw => flush()
208 private val timer = new Timer("session_actor.receiver", true)
209 timer.schedule(new TimerTask { def run = flush }, message_delay.ms, message_delay.ms)
211 def cancel() { timer.cancel() }
214 var prover: Option[Isabelle_Process with Protocol] = None
217 /* delayed command changes */
219 object delay_commands_changed
221 private var changed_nodes: Set[Document.Node.Name] = Set.empty
222 private var changed_commands: Set[Command] = Set.empty
223 private def changed: Boolean = !changed_nodes.isEmpty || !changed_commands.isEmpty
225 private var flush_time: Option[Long] = None
227 def flush_timeout: Long =
230 case Some(time) => (time - System.currentTimeMillis()) max 0
236 commands_changed_buffer ! Session.Commands_Changed(changed_nodes, changed_commands)
237 changed_nodes = Set.empty
238 changed_commands = Set.empty
242 def invoke(command: Command)
244 changed_nodes += command.node_name
245 changed_commands += command
246 val now = System.currentTimeMillis()
248 case None => flush_time = Some(now + output_delay.ms)
249 case Some(time) => if (now >= time) flush()
257 def update_perspective(name: Document.Node.Name, text_perspective: Text.Perspective)
259 val previous = global_state().tip_version
260 val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
262 val text_edits: List[Document.Edit_Text] =
263 List((name, Document.Node.Perspective(text_perspective)))
265 global_state.change_yield(
266 _.continue_history(Future.value(previous), text_edits, Future.value(version)))
268 val assignment = global_state().the_assignment(previous).check_finished
269 global_state.change(_.define_version(version, assignment))
270 global_state.change_yield(_.assign(version.id, Document.no_assign))
272 prover.get.update_perspective(previous.id, version.id, name, perspective)
278 def handle_edits(name: Document.Node.Name,
279 header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
282 val syntax = current_syntax()
283 val previous = global_state().history.tip.version
285 prover.get.cancel_execution()
287 val text_edits = header_edit(name, header) :: edits.map(edit => (name, edit))
288 val version = Future.promise[Document.Version]
289 val change = global_state.change_yield(_.continue_history(previous, text_edits, version))
291 change_parser ! Text_Edits(syntax, name, previous, text_edits, version)
296 /* exec state assignment */
298 def handle_assign(id: Document.Version_ID, assign: Document.Assign)
301 val cmds = global_state.change_yield(_.assign(id, assign))
302 for (cmd <- cmds) delay_commands_changed.invoke(cmd)
307 /* removed versions */
309 def handle_removed(removed: List[Document.Version_ID])
312 global_state.change(_.removed_versions(removed))
317 /* resulting changes */
319 def handle_change(change: Change_Node)
322 val previous = change.previous
323 val version = change.version
324 val name = change.name
325 val doc_edits = change.doc_edits
327 def id_command(command: Command)
329 if (!global_state().defined_command(command.id)) {
330 global_state.change(_.define_command(command))
331 prover.get.define_command(command)
336 edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
339 val assignment = global_state().the_assignment(previous).check_finished
340 global_state.change(_.define_version(version, assignment))
341 prover.get.update(previous.id, version.id, doc_edits)
348 def handle_result(result: Isabelle_Process.Result)
351 def bad_result(result: Isabelle_Process.Result)
354 System.err.println("Ignoring prover result: " + result.message.toString)
357 result.properties match {
359 case Position.Id(state_id) if !result.is_raw =>
361 val st = global_state.change_yield(_.accumulate(state_id, result.message))
362 delay_commands_changed.invoke(st.command)
365 case _: Document.State.Fail => bad_result(result)
368 case Isabelle_Markup.Assign_Execs if result.is_raw =>
369 XML.content(result.body).mkString match {
370 case Protocol.Assign(id, assign) =>
371 try { handle_assign(id, assign) }
372 catch { case _: Document.State.Fail => bad_result(result) }
373 case _ => bad_result(result)
375 // FIXME separate timeout event/message!?
376 if (prover.isDefined && System.currentTimeMillis() > prune_next) {
377 val old_versions = global_state.change_yield(_.prune_history(prune_size))
378 if (!old_versions.isEmpty) prover.get.remove_versions(old_versions)
379 prune_next = System.currentTimeMillis() + prune_delay.ms
382 case Isabelle_Markup.Removed_Versions if result.is_raw =>
383 XML.content(result.body).mkString match {
384 case Protocol.Removed(removed) =>
385 try { handle_removed(removed) }
386 catch { case _: Document.State.Fail => bad_result(result) }
387 case _ => bad_result(result)
390 case Isabelle_Markup.Invoke_Scala(name, id) if result.is_raw =>
392 val arg = XML.content(result.body).mkString
393 val (tag, res) = Invoke_Scala.method(name, arg)
394 prover.get.invoke_scala(id, tag, res)
397 case Isabelle_Markup.Cancel_Scala(id) if result.is_raw =>
398 System.err.println("cancel_scala " + id) // FIXME actually cancel JVM task
400 case Isabelle_Markup.Ready if result.is_raw =>
401 // FIXME move to ML side (!?)
402 syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
403 syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
404 phase = Session.Ready
406 case Isabelle_Markup.Loaded_Theory(name) if result.is_raw =>
407 thy_load.register_thy(name)
409 case Isabelle_Markup.Command_Decl(name, kind) if result.is_raw =>
410 syntax += (name, kind)
412 case Isabelle_Markup.Keyword_Decl(name) if result.is_raw =>
416 if (result.is_syslog) {
417 reverse_syslog ::= result.message
418 if (result.is_exit && phase == Session.Startup) phase = Session.Failed
419 else if (result.is_exit) phase = Session.Inactive
421 else if (result.is_stdout) { }
422 else bad_result(result)
433 receiveWithin(delay_commands_changed.flush_timeout) {
434 case TIMEOUT => delay_commands_changed.flush()
436 case Start(timeout, args) if prover.isEmpty =>
437 if (phase == Session.Inactive || phase == Session.Failed) {
438 phase = Session.Startup
439 prover = Some(new Isabelle_Process(timeout, receiver.invoke _, args) with Protocol)
443 if (phase == Session.Ready) {
444 global_state.change(_ => Document.State.init) // FIXME event bus!?
445 phase = Session.Shutdown
448 phase = Session.Inactive
454 case Cancel_Execution if prover.isDefined =>
455 prover.get.cancel_execution()
457 case Init_Node(name, header, perspective, text) if prover.isDefined =>
458 // FIXME compare with existing node
459 handle_edits(name, header,
460 List(Document.Node.Clear(),
461 Document.Node.Edits(List(Text.Edit.insert(0, text))),
462 Document.Node.Perspective(perspective)))
465 case Edit_Node(name, header, perspective, text_edits) if prover.isDefined =>
466 if (text_edits.isEmpty && global_state().tip_stable &&
467 perspective.range.stop <= global_state().last_exec_offset(name))
468 update_perspective(name, perspective)
470 handle_edits(name, header,
471 List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
474 case Messages(msgs) =>
476 case input: Isabelle_Process.Input =>
477 protocol_messages.event(input)
479 case result: Isabelle_Process.Result =>
480 handle_result(result)
481 if (result.is_syslog) syslog_messages.event(result)
482 if (result.is_stdout || result.is_stderr) raw_output_messages.event(result)
483 protocol_messages.event(result)
486 case change: Change_Node
487 if prover.isDefined && global_state().is_assigned(change.previous) =>
488 handle_change(change)
490 case bad if !bad.isInstanceOf[Change_Node] =>
491 System.err.println("session_actor: ignoring bad message " + bad)
500 def start(timeout: Time, args: List[String])
501 { session_actor ! Start(timeout, args) }
503 def start(args: List[String]) { start (Time.seconds(25), args) }
505 def stop() { commands_changed_buffer !? Stop; change_parser !? Stop; session_actor !? Stop }
507 def cancel_execution() { session_actor ! Cancel_Execution }
509 def init_node(name: Document.Node.Name,
510 header: Document.Node_Header, perspective: Text.Perspective, text: String)
511 { session_actor !? Init_Node(name, header, perspective, text) }
513 def edit_node(name: Document.Node.Name,
514 header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
515 { session_actor !? Edit_Node(name, header, perspective, edits) }