--- a/src/Pure/System/session.scala Sat Jul 09 13:29:33 2011 +0200
+++ b/src/Pure/System/session.scala Sat Jul 09 16:53:19 2011 +0200
@@ -16,7 +16,7 @@
object Session
{
- /* abstract file store */
+ /* file store */
abstract class File_Store
{
@@ -26,6 +26,7 @@
/* events */
+ //{{{
case object Global_Settings
case object Perspective
case object Assignment
@@ -37,6 +38,7 @@
case object Failed extends Phase
case object Ready extends Phase
case object Shutdown extends Phase // transient
+ //}}}
}
@@ -44,33 +46,29 @@
{
/* real time parameters */ // FIXME properties or settings (!?)
- // user input (e.g. text edits, cursor movement)
- val input_delay = Time.seconds(0.3)
-
- // prover output (markup, common messages)
- val output_delay = Time.seconds(0.1)
-
- // GUI layout updates
- val update_delay = Time.seconds(0.5)
+ val input_delay = Time.seconds(0.3) // user input (e.g. text edits, cursor movement)
+ val output_delay = Time.seconds(0.1) // prover output (markup, common messages)
+ val update_delay = Time.seconds(0.5) // GUI layout updates
/* pervasive event buses */
- val phase_changed = new Event_Bus[Session.Phase]
val global_settings = new Event_Bus[Session.Global_Settings.type]
- val raw_messages = new Event_Bus[Isabelle_Process.Result]
- val commands_changed = new Event_Bus[Session.Commands_Changed]
val perspective = new Event_Bus[Session.Perspective.type]
val assignments = new Event_Bus[Session.Assignment.type]
+ val commands_changed = new Event_Bus[Session.Commands_Changed]
+ val phase_changed = new Event_Bus[Session.Phase]
+ val raw_messages = new Event_Bus[Isabelle_Process.Result]
+
/** buffered command changes (delay_first discipline) **/
+ //{{{
private case object Stop
private val (_, command_change_buffer) =
Simple_Thread.actor("command_change_buffer", daemon = true)
- //{{{
{
var changed: Set[Command] = Set()
var flush_time: Option[Long] = None
@@ -115,7 +113,9 @@
/* global state */
- @volatile var loaded_theories: Set[String] = Set()
+ @volatile var verbose: Boolean = false
+
+ @volatile private var loaded_theories: Set[String] = Set()
@volatile private var syntax = new Outer_Syntax
def current_syntax(): Outer_Syntax = syntax
@@ -124,17 +124,20 @@
def syslog(): String = reverse_syslog.reverse.map(msg => XML.content(msg).mkString).mkString("\n")
@volatile private var _phase: Session.Phase = Session.Inactive
- def phase = _phase
private def phase_=(new_phase: Session.Phase)
{
_phase = new_phase
phase_changed.event(new_phase)
}
+ def phase = _phase
def is_ready: Boolean = phase == Session.Ready
private val global_state = new Volatile(Document.State.init)
def current_state(): Document.State = global_state.peek()
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+ current_state().snapshot(name, pending_edits)
+
/* theory files */
@@ -158,12 +161,10 @@
/* actor messages */
- private case object Interrupt_Prover
- private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+ private case class Start(timeout: Time, args: List[String])
+ private case object Interrupt
private case class Init_Node(name: String, header: Document.Node.Header, text: String)
- private case class Start(timeout: Time, args: List[String])
-
- var verbose: Boolean = false
+ private case class Edit_Node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
private val (_, session_actor) = Simple_Thread.actor("session_actor", daemon = true)
{
@@ -171,7 +172,24 @@
var prover: Option[Isabelle_Process with Isar_Document] = None
- /* document changes */
+ /* incoming edits */
+
+ def handle_edits(headers: List[Document.Node.Header], edits: List[Document.Edit_Text])
+ //{{{
+ {
+ val syntax = current_syntax()
+ val previous = current_state().history.tip.version
+ val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
+ val change = global_state.change_yield(_.extend_history(previous, edits, result))
+
+ change.version.map(_ => {
+ assignments.await { current_state().is_assigned(previous.get_finished) }
+ this_actor ! change })
+ }
+ //}}}
+
+
+ /* resulting changes */
def handle_change(change: Document.Change)
//{{{
@@ -179,7 +197,7 @@
val previous = change.previous.get_finished
val (node_edits, version) = change.result.get_finished
- var former_assignment = global_state.peek().the_assignment(previous).get_finished
+ var former_assignment = current_state().the_assignment(previous).get_finished
for {
(name, Some(cmd_edits)) <- node_edits
(prev, None) <- cmd_edits
@@ -198,7 +216,7 @@
c2 match {
case None => None
case Some(command) =>
- if (global_state.peek().lookup_command(command.id).isEmpty) {
+ if (current_state().lookup_command(command.id).isEmpty) {
global_state.change(_.define_command(command))
prover.get.define_command(command.id, Symbol.encode(command.source))
}
@@ -216,15 +234,15 @@
/* prover results */
- def bad_result(result: Isabelle_Process.Result)
- {
- if (verbose)
- System.err.println("Ignoring prover result: " + result.message.toString)
- }
-
def handle_result(result: Isabelle_Process.Result)
//{{{
{
+ def bad_result(result: Isabelle_Process.Result)
+ {
+ if (verbose)
+ System.err.println("Ignoring prover result: " + result.message.toString)
+ }
+
result.properties match {
case Position.Id(state_id) =>
try {
@@ -236,7 +254,7 @@
if (result.is_syslog) {
reverse_syslog ::= result.message
if (result.is_ready) {
- // FIXME move to ML side
+ // FIXME move to ML side (!?)
syntax += ("hence", Keyword.PRF_ASM_GOAL, "then have")
syntax += ("thus", Keyword.PRF_ASM_GOAL, "then show")
phase = Session.Ready
@@ -268,47 +286,12 @@
//}}}
- def edit_version(edits: List[Document.Edit_Text])
- //{{{
- {
- val previous = global_state.peek().history.tip.version
- val syntax = current_syntax()
- val result = Future.fork { Thy_Syntax.text_edits(syntax, previous.join, edits) }
- val change = global_state.change_yield(_.extend_history(previous, edits, result))
-
- change.version.map(_ => {
- assignments.await { global_state.peek().is_assigned(previous.get_finished) }
- this_actor ! change })
- }
- //}}}
-
-
/* main loop */
+ //{{{
var finished = false
while (!finished) {
receive {
- case Interrupt_Prover =>
- prover.map(_.interrupt)
-
- case Edit_Node(name, header, text_edits) if prover.isDefined =>
- val node_name = (header.master_dir + Path.basic(name)).implode // FIXME
- edit_version(List((node_name, Some(text_edits))))
- reply(())
-
- case Init_Node(name, header, text) if prover.isDefined =>
- // FIXME compare with existing node
- val node_name = (header.master_dir + Path.basic(name)).implode // FIXME
- edit_version(List(
- (node_name, None),
- (node_name, Some(List(Text.Edit.insert(0, text))))))
- reply(())
-
- case change: Document.Change if prover.isDefined =>
- handle_change(change)
-
- case result: Isabelle_Process.Result => handle_result(result)
-
case Start(timeout, args) if prover.isEmpty =>
if (phase == Session.Inactive || phase == Session.Failed) {
phase = Session.Startup
@@ -325,32 +308,48 @@
finished = true
reply(())
+ case Interrupt =>
+ prover.map(_.interrupt)
+
+ case Edit_Node(name, header, text_edits) if prover.isDefined =>
+ val node_name = (header.master_dir + Path.basic(name)).implode // FIXME
+ handle_edits(List(header), List((node_name, Some(text_edits))))
+ reply(())
+
+ case Init_Node(name, header, text) if prover.isDefined =>
+ // FIXME compare with existing node
+ val node_name = (header.master_dir + Path.basic(name)).implode // FIXME
+ handle_edits(List(header),
+ List(
+ (node_name, None),
+ (node_name, Some(List(Text.Edit.insert(0, text))))))
+ reply(())
+
+ case change: Document.Change if prover.isDefined =>
+ handle_change(change)
+
+ case result: Isabelle_Process.Result =>
+ handle_result(result)
+
case bad if prover.isDefined =>
System.err.println("session_actor: ignoring bad message " + bad)
}
}
+ //}}}
}
-
- /** main methods **/
+ /* actions */
def start(timeout: Time, args: List[String]) { session_actor ! Start(timeout, args) }
def stop() { command_change_buffer !? Stop; session_actor !? Stop }
- def interrupt() { session_actor ! Interrupt_Prover }
-
- def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
- {
- session_actor !? Edit_Node(name, header, edits)
- }
+ def interrupt() { session_actor ! Interrupt }
def init_node(name: String, header: Document.Node.Header, text: String)
- {
- session_actor !? Init_Node(name, header, text)
- }
+ { session_actor !? Init_Node(name, header, text) }
- def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
- global_state.peek().snapshot(name, pending_edits)
+ def edit_node(name: String, header: Document.Node.Header, edits: List[Text.Edit])
+ { session_actor !? Edit_Node(name, header, edits) }
}