1 /* Title: Pure/System/session.scala
3 Options: :folding=explicit:collapseFolds=1:
5 Main Isabelle/Scala session, potentially with running prover process.
10 import java.lang.System
12 import scala.actors.TIMEOUT
13 import scala.actors.Actor
14 import scala.actors.Actor._
21 abstract class File_Store
23 def append(master_dir: String, path: Path): String
24 def require(file: String): Unit
31 case object Global_Settings
32 case object Perspective
33 case object Assignment
34 case class Commands_Changed(set: Set[Command])
36 sealed abstract class Phase
37 case object Inactive extends Phase
38 case object Startup extends Phase // transient
39 case object Failed extends Phase
40 case object Ready extends Phase
41 case object Shutdown extends Phase // transient
46 class Session(val file_store: Session.File_Store)
48 /* real time parameters */ // FIXME properties or settings (!?)
50 val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
51 val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
52 val update_delay = Time.seconds(0.5) // GUI layout updates
53 val load_delay = Time.seconds(0.5) // file load operations (new buffers etc.)
56 /* pervasive event buses */
58 val global_settings = new Event_Bus[Session.Global_Settings.type]
59 val perspective = new Event_Bus[Session.Perspective.type]
60 val assignments = new Event_Bus[Session.Assignment.type]
61 val commands_changed = new Event_Bus[Session.Commands_Changed]
62 val phase_changed = new Event_Bus[Session.Phase]
63 val raw_messages = new Event_Bus[Isabelle_Process.Message]
67 /** buffered command changes (delay_first discipline) **/
70 private case object Stop
72 private val (_, command_change_buffer) =
73 Simple_Thread.actor("command_change_buffer", daemon = true)
75 var changed: Set[Command] = Set()
76 var flush_time: Option[Long] = None
78 def flush_timeout: Long =
81 case Some(time) => (time - System.currentTimeMillis()) max 0
86 if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
93 val now = System.currentTimeMillis()
95 case None => flush_time = Some(now + output_delay.ms)
96 case Some(time) => if (now >= time) flush()
102 receiveWithin(flush_timeout) {
103 case command: Command => changed += command; invoke()
104 case TIMEOUT => flush()
105 case Stop => finished = true; reply(())
106 case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
114 /** main protocol actor **/
118 @volatile var verbose: Boolean = false
120 @volatile private var loaded_theories: Set[String] = Set()
122 @volatile private var syntax = new Outer_Syntax
123 def current_syntax(): Outer_Syntax = syntax
125 @volatile private var reverse_syslog = List[XML.Elem]()
126 def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
128 @volatile private var _phase: Session.Phase = Session.Inactive
129 private def phase_=(new_phase: Session.Phase)
132 phase_changed.event(new_phase)
135 def is_ready: Boolean = phase == Session.Ready
137 private val global_state = new Volatile(Document.State.init)
138 def current_state(): Document.State = global_state()
140 def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
141 global_state().snapshot(name, pending_edits)
146 val thy_load = new Thy_Load
148 override def is_loaded(name: String): Boolean =
149 loaded_theories.contains(name)
151 override def check_thy(dir: Path, name: String): (String, Thy_Header) =
153 val file = Isabelle_System.platform_file(dir + Thy_Header.thy_path(name))
154 if (!file.exists || !file.isFile) error("No such file: " + quote(file.toString))
155 val text = Standard_System.read_file(file)
156 val header = Thy_Header.read(text)
161 val thy_info = new Thy_Info(thy_load)
163 def header_edit(name: String, master_dir: String,
164 header: Document.Node_Header): Document.Edit_Text =
166 def norm_import(s: String): String =
168 val thy_name = Thy_Header.base_name(s)
169 if (thy_load.is_loaded(thy_name)) thy_name
170 else file_store.append(master_dir, Thy_Header.thy_path(Path.explode(s)))
172 def norm_use(s: String): String =
173 file_store.append(master_dir, Path.explode(s))
175 val header1: Document.Node_Header =
177 case Exn.Res(Thy_Header(thy_name, _, _))
178 if (thy_load.is_loaded(thy_name)) =>
179 Exn.Exn(ERROR("Attempt to update loaded theory " + quote(thy_name)))
180 case _ => Document.Node.norm_header(norm_import, norm_use, header)
182 (name, Document.Node.Header(header1))
188 private case class Start(timeout: Time, args: List[String])
189 private case object Interrupt
190 private case class Check_Loaded_Files(ask: List[String] => Boolean)
191 private case class Init_Node(name: String, master_dir: String,
192 header: Document.Node_Header, perspective: Text.Perspective, text: String)
193 private case class Edit_Node(name: String, master_dir: String,
194 header: Document.Node_Header, perspective: Text.Perspective, edits: List[Text.Edit])
195 private case class Change_Node(
197 doc_edits: List[Document.Edit_Command],
198 previous: Document.Version,
199 version: Document.Version)
201 private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
203 val this_actor = self
204 var prover: Option[Isabelle_Process with Isar_Document] = None
209 def update_perspective(name: String, text_perspective: Text.Perspective)
211 val previous = global_state().tip_version
212 val (perspective, version) = Thy_Syntax.edit_perspective(previous, name, text_perspective)
214 val text_edits: List[Document.Edit_Text] =
215 List((name, Document.Node.Perspective(text_perspective)))
217 global_state.change_yield(
218 _.continue_history(Future.value(previous), text_edits, Future.value(version)))
220 val assignment = global_state().the_assignment(previous).check_finished
221 global_state.change(_.define_version(version, assignment))
222 global_state.change_yield(_.assign(version.id, Document.no_assign))
224 prover.get.update_perspective(previous.id, version.id, name, perspective)
230 def handle_edits(name: String, master_dir: String,
231 header: Document.Node_Header, edits: List[Document.Node.Edit[Text.Edit, Text.Perspective]])
234 val syntax = current_syntax()
235 val previous = global_state().history.tip.version
237 val text_edits = header_edit(name, master_dir, header) :: edits.map(edit => (name, edit))
238 val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, text_edits) }
240 global_state.change_yield(_.continue_history(previous, text_edits, result.map(_._2)))
243 case (doc_edits, _) =>
244 assignments.await { global_state().is_assigned(previous.get_finished) }
245 this_actor ! Change_Node(name, doc_edits, previous.join, change.version.join)
251 /* exec state assignment */
253 def handle_assign(id: Document.Version_ID, assign: Document.Assign)
256 val cmds = global_state.change_yield(_.assign(id, assign))
257 for (cmd <- cmds) command_change_buffer ! cmd
258 assignments.event(Session.Assignment)
263 /* resulting changes */
265 def handle_change(change: Change_Node)
268 val previous = change.previous
269 val version = change.version
270 val name = change.name
271 val doc_edits = change.doc_edits
273 def id_command(command: Command)
275 if (global_state().lookup_command(command.id).isEmpty) {
276 global_state.change(_.define_command(command))
277 prover.get.define_command(command.id, Symbol.encode(command.source))
282 edit foreach { case (c1, c2) => c1 foreach id_command; c2 foreach id_command }
285 val assignment = global_state().the_assignment(previous).check_finished
286 global_state.change(_.define_version(version, assignment))
287 prover.get.update(previous.id, version.id, doc_edits)
294 def handle_result(result: Isabelle_Process.Result)
297 def bad_result(result: Isabelle_Process.Result)
300 System.err.println("Ignoring prover result: " + result.message.toString)
303 result.properties match {
304 case Position.Id(state_id) if !result.is_raw =>
306 val st = global_state.change_yield(_.accumulate(state_id, result.message))
307 command_change_buffer ! st.command
310 case _: Document.State.Fail => bad_result(result)
312 case Markup.Invoke_Scala(name, id) if result.is_raw =>
314 val arg = XML.content(result.body).mkString
315 val (tag, res) = Invoke_Scala.method(name, arg)
316 prover.get.invoke_scala(id, tag, res)
318 case Markup.Cancel_Scala(id) =>
319 System.err.println("cancel_scala " + id) // FIXME cancel JVM task
321 if (result.is_syslog) {
322 reverse_syslog ::= result.message
323 if (result.is_ready) {
324 // FIXME move to ML side (!?)
325 syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
326 syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
327 phase = Session.Ready
329 else if (result.is_exit && phase == Session.Startup) phase = Session.Failed
330 else if (result.is_exit) phase = Session.Inactive
332 else if (result.is_stdout) { }
333 else if (result.is_status) {
335 case List(Isar_Document.Assign(id, assign)) =>
336 try { handle_assign(id, assign) }
337 catch { case _: Document.State.Fail => bad_result(result) }
338 case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
339 case List(Keyword.Keyword_Decl(name)) => syntax += name
340 case List(Thy_Info.Loaded_Theory(name)) => loaded_theories += name
341 case _ => bad_result(result)
344 else bad_result(result)
356 case Start(timeout, args) if prover.isEmpty =>
357 if (phase == Session.Inactive || phase == Session.Failed) {
358 phase = Session.Startup
359 prover = Some(new Isabelle_Process(timeout, this_actor, args:_*) with Isar_Document)
363 if (phase == Session.Ready) {
364 global_state.change(_ => Document.State.init) // FIXME event bus!?
365 phase = Session.Shutdown
368 phase = Session.Inactive
373 case Interrupt if prover.isDefined =>
376 case Check_Loaded_Files(ask) => // FIXME
378 case Init_Node(name, master_dir, header, perspective, text) if prover.isDefined =>
379 // FIXME compare with existing node
380 handle_edits(name, master_dir, header,
381 List(Document.Node.Clear(),
382 Document.Node.Edits(List(Text.Edit.insert(0, text))),
383 Document.Node.Perspective(perspective)))
386 case Edit_Node(name, master_dir, header, perspective, text_edits) if prover.isDefined =>
387 if (text_edits.isEmpty && global_state().tip_stable &&
388 perspective.range.stop <= global_state().last_exec_offset(name))
389 update_perspective(name, perspective)
391 handle_edits(name, master_dir, header,
392 List(Document.Node.Edits(text_edits), Document.Node.Perspective(perspective)))
395 case change: Change_Node if prover.isDefined =>
396 handle_change(change)
398 case input: Isabelle_Process.Input =>
399 raw_messages.event(input)
401 case result: Isabelle_Process.Result =>
402 handle_result(result)
403 raw_messages.event(result)
405 case bad => System.err.println("session_actor: ignoring bad message " + bad)
414 def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
416 def stop() { command_change_buffer !? Stop; session_actor !? Stop }
418 def interrupt() { session_actor ! Interrupt }
420 def check_loaded_files(ask: List[String] => Boolean)
422 session_actor ! Check_Loaded_Files(ask)
425 // FIXME simplify signature
426 def init_node(name: String, master_dir: String,
427 header: Document.Node_Header, perspective: Text.Perspective, text: String)
428 { session_actor !? Init_Node(name, master_dir, header, perspective, text) }
430 // FIXME simplify signature
431 def edit_node(name: String, master_dir: String, header: Document.Node_Header,
432 perspective: Text.Perspective, edits: List[Text.Edit])
433 { session_actor !? Edit_Node(name, master_dir, header, perspective, edits) }