# HG changeset patch # User wenzelm # Date 1283009258 -7200 # Node ID 4df7b76249a0bb56f57fb27753d566e3d83c53c8 # Parent ec75dc58688b4cd813ef9b0b38acce1b61afa365 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; diff -r ec75dc58688b -r 4df7b76249a0 src/Pure/PIDE/document.scala --- 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)) + } } } } diff -r ec75dc58688b -r 4df7b76249a0 src/Pure/System/session.scala --- 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) }