include Document.History in Document.State -- just one universal session state maintained by main actor;
Session.command_change_buffer: thread actor ensures asynchronous dispatch;
misc tuning;
--- a/src/Pure/PIDE/document.scala Sat Aug 28 17:20:53 2010 +0200
+++ b/src/Pure/PIDE/document.scala Sat Aug 28 17:27:38 2010 +0200
@@ -116,7 +116,25 @@
}
- /* history navigation and persistent snapshots */
+ /* history navigation */
+
+ object History
+ {
+ val init = new History(List(Change.init))
+ }
+
+ // FIXME pruning, purging of state
+ class History(val undo_list: List[Change])
+ {
+ require(!undo_list.isEmpty)
+
+ def tip: Change = undo_list.head
+ def +(change: Change): History = new History(change :: undo_list)
+ }
+
+
+
+ /** global state -- document structure, execution process, editing history **/
abstract class Snapshot
{
@@ -131,52 +149,6 @@
def revert(range: Text.Range): Text.Range = range.map(revert(_))
}
- object History
- {
- val init = new History(List(Change.init))
- }
-
- // FIXME pruning, purging of state
- class History(undo_list: List[Change])
- {
- require(!undo_list.isEmpty)
-
- def tip: Change = undo_list.head
- def +(ch: Change): History = new History(ch :: undo_list)
-
- def snapshot(name: String, pending_edits: List[Text.Edit], state_snapshot: State): Snapshot =
- {
- val found_stable = undo_list.find(change =>
- change.is_finished && state_snapshot.is_assigned(change.current.join))
- require(found_stable.isDefined)
- val stable = found_stable.get
- val latest = undo_list.head
-
- val edits =
- (pending_edits /: undo_list.takeWhile(_ != stable))((edits, change) =>
- (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
- lazy val reverse_edits = edits.reverse
-
- new Snapshot
- {
- val version = stable.current.join
- val node = version.nodes(name)
- val is_outdated = !(pending_edits.isEmpty && latest == stable)
- def lookup_command(id: Command_ID): Option[Command] = state_snapshot.lookup_command(id)
- def state(command: Command): Command.State =
- try { state_snapshot.command_state(version, command) }
- catch { case _: State.Fail => command.empty_state }
-
- def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
- def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- }
- }
- }
-
-
-
- /** global state -- document structure and execution process **/
-
object State
{
class Fail(state: State) extends Exception
@@ -202,7 +174,8 @@
val commands: Map[Command_ID, Command.State] = Map(),
val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
val assignments: Map[Version, State.Assignment] = Map(),
- val disposed: Set[ID] = Set()) // FIXME unused!?
+ val disposed: Set[ID] = Set(), // FIXME unused!?
+ val history: History = History.init)
{
private def fail[A]: A = throw new State.Fail(this)
@@ -265,11 +238,44 @@
case None => false
}
- def command_state(version: Version, command: Command): Command.State =
+ def extend_history(previous: Future[Version],
+ edits: List[Node_Text_Edit],
+ result: Future[(List[Edit[Command]], Version)]): (Change, State) =
+ {
+ val change = new Change(previous, edits, result)
+ (change, copy(history = history + change))
+ }
+
+
+ // persistent user-view
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Snapshot =
{
- val assgn = the_assignment(version)
- require(assgn.is_finished)
- the_exec_state(assgn.join.getOrElse(command, fail))
+ val found_stable = history.undo_list.find(change =>
+ change.is_finished && is_assigned(change.current.join))
+ require(found_stable.isDefined)
+ val stable = found_stable.get
+ val latest = history.undo_list.head
+
+ val edits =
+ (pending_edits /: history.undo_list.takeWhile(_ != stable))((edits, change) =>
+ (for ((a, eds) <- change.edits if a == name) yield eds).flatten ::: edits)
+ lazy val reverse_edits = edits.reverse
+
+ new Snapshot
+ {
+ val version = stable.current.join
+ val node = version.nodes(name)
+ val is_outdated = !(pending_edits.isEmpty && latest == stable)
+
+ def lookup_command(id: Command_ID): Option[Command] = State.this.lookup_command(id)
+
+ def state(command: Command): Command.State =
+ try { the_exec_state(the_assignment(version).join.getOrElse(command, fail)) }
+ catch { case _: State.Fail => command.empty_state }
+
+ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
+ def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
+ }
}
}
}
--- a/src/Pure/System/session.scala Sat Aug 28 17:20:53 2010 +0200
+++ b/src/Pure/System/session.scala Sat Aug 28 17:27:38 2010 +0200
@@ -57,17 +57,64 @@
- /** main actor **/
+ /** buffered command changes (delay_first discipline) **/
+
+ private case object Stop
+
+ private val command_change_buffer = Simple_Thread.actor("command_change_buffer", daemon = true)
+ //{{{
+ {
+ import scala.compat.Platform.currentTime
+
+ var changed: Set[Command] = Set()
+ var flush_time: Option[Long] = None
+
+ def flush_timeout: Long =
+ flush_time match {
+ case None => 5000L
+ case Some(time) => (time - currentTime) max 0
+ }
+
+ def flush()
+ {
+ if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
+ changed = Set()
+ flush_time = None
+ }
+
+ def invoke()
+ {
+ val now = currentTime
+ flush_time match {
+ case None => flush_time = Some(now + output_delay)
+ case Some(time) => if (now >= time) flush()
+ }
+ }
+
+ var finished = false
+ while (!finished) {
+ receiveWithin(flush_timeout) {
+ case command: Command => changed += command; invoke()
+ case TIMEOUT => flush()
+ case Stop => finished = true
+ case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
+ }
+ }
+ }
+ //}}}
+
+
+
+ /** main protocol actor **/
@volatile private var syntax = new Outer_Syntax(system.symbols)
def current_syntax(): Outer_Syntax = syntax
- @volatile private var global_state = Document.State.init
- private def change_state(f: Document.State => Document.State) { global_state = f(global_state) }
- def current_state(): Document.State = global_state
+ private val global_state = new Volatile(Document.State.init)
+ def current_state(): Document.State = global_state.peek()
+ private case class Edit_Version(edits: List[Document.Node_Text_Edit])
private case class Started(timeout: Int, args: List[String])
- private case object Stop
private val session_actor = Simple_Thread.actor("session_actor", daemon = true)
{
@@ -84,7 +131,7 @@
val previous = change.previous.join
val (node_edits, current) = change.result.join
- var former_assignment = current_state().the_assignment(previous).join
+ var former_assignment = global_state.peek().the_assignment(previous).join
for {
(name, Some(cmd_edits)) <- node_edits
(prev, None) <- cmd_edits
@@ -103,8 +150,8 @@
c2 match {
case None => None
case Some(command) =>
- if (current_state().lookup_command(command.id).isEmpty) {
- change_state(_.define_command(command))
+ if (global_state.peek().lookup_command(command.id).isEmpty) {
+ global_state.change(_.define_command(command))
prover.define_command(command.id, system.symbols.encode(command.source))
}
Some(command.id)
@@ -113,7 +160,7 @@
}
(name -> Some(ids))
}
- change_state(_.define_version(current, former_assignment))
+ global_state.change(_.define_version(current, former_assignment))
prover.edit_version(previous.id, current.id, id_edits)
}
//}}}
@@ -134,16 +181,15 @@
result.properties match {
case Position.Id(state_id) =>
try {
- val (st, state) = global_state.accumulate(state_id, result.message)
- global_state = state
- indicate_command_change(st.command)
+ val st = global_state.change_yield(_.accumulate(state_id, result.message))
+ command_change_buffer ! st.command
}
catch { case _: Document.State.Fail => bad_result(result) }
case _ =>
if (result.is_status) {
result.body match {
case List(Isar_Document.Assign(id, edits)) =>
- try { change_state(_.assign(id, edits)) }
+ try { global_state.change(_.assign(id, edits)) }
catch { case _: Document.State.Fail => bad_result(result) }
case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -202,6 +248,19 @@
var finished = false
while (!finished) {
receive {
+ case Edit_Version(edits) =>
+ val previous = global_state.peek().history.tip.current
+ val result = Future.fork { Thy_Syntax.text_edits(Session.this, previous.join, edits) }
+ val change = global_state.change_yield(_.extend_history(previous, edits, result))
+ val this_actor = self; result.map(_ => this_actor ! change)
+ reply(())
+
+ case change: Document.Change if prover != null =>
+ handle_change(change)
+
+ case result: Isabelle_Process.Result =>
+ handle_result(result)
+
case Started(timeout, args) =>
if (prover == null) {
prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -219,12 +278,6 @@
finished = true
}
- case change: Document.Change if prover != null =>
- handle_change(change)
-
- case result: Isabelle_Process.Result =>
- handle_result(result)
-
case TIMEOUT => // FIXME clarify!
case bad if prover != null =>
@@ -235,95 +288,15 @@
- /** buffered command changes (delay_first discipline) **/
-
- private val command_change_buffer = actor
- //{{{
- {
- import scala.compat.Platform.currentTime
-
- var changed: Set[Command] = Set()
- var flush_time: Option[Long] = None
-
- def flush_timeout: Long =
- flush_time match {
- case None => 5000L
- case Some(time) => (time - currentTime) max 0
- }
-
- def flush()
- {
- if (!changed.isEmpty) commands_changed.event(Session.Commands_Changed(changed))
- changed = Set()
- flush_time = None
- }
-
- def invoke()
- {
- val now = currentTime
- flush_time match {
- case None => flush_time = Some(now + output_delay)
- case Some(time) => if (now >= time) flush()
- }
- }
-
- loop {
- reactWithin(flush_timeout) {
- case command: Command => changed += command; invoke()
- case TIMEOUT => flush()
- case bad => System.err.println("command_change_buffer: ignoring bad message " + bad)
- }
- }
- }
- //}}}
-
- def indicate_command_change(command: Command)
- {
- command_change_buffer ! command
- }
-
-
-
- /** editor history **/
-
- private case class Edit_Version(edits: List[Document.Node_Text_Edit])
-
- @volatile private var history = Document.History.init
-
- def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
- history.snapshot(name, pending_edits, current_state())
-
- private val editor_history = actor
- {
- loop {
- react {
- case Edit_Version(edits) =>
- val prev = history.tip.current
- val result =
- // FIXME potential denial-of-service concerning worker pool (!?!?)
- isabelle.Future.fork {
- val previous = prev.join
- val former_assignment = current_state().the_assignment(previous).join // FIXME async!?
- Thy_Syntax.text_edits(Session.this, previous, edits)
- }
- val change = new Document.Change(prev, edits, result)
- history += change
- change.current.map(_ => session_actor ! change)
- reply(())
-
- case bad => System.err.println("editor_model: ignoring bad message " + bad)
- }
- }
- }
-
-
-
/** main methods **/
def started(timeout: Int, args: List[String]): Option[String] =
(session_actor !? Started(timeout, args)).asInstanceOf[Option[String]]
- def stop() { session_actor ! Stop }
+ def stop() { command_change_buffer ! Stop; session_actor ! Stop }
+
+ def edit_version(edits: List[Document.Node_Text_Edit]) { session_actor !? Edit_Version(edits) }
- def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
+ def snapshot(name: String, pending_edits: List[Text.Edit]): Document.Snapshot =
+ global_state.peek().snapshot(name, pending_edits)
}