unified Command and Command_State, eliminated separate Accumulator;
Command.finish_static: idempotent transition from static to dynamic mode, taking snapshot of final state (which will never change later);
--- a/src/Tools/jEdit/src/proofdocument/command.scala Wed Dec 30 18:22:10 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala Wed Dec 30 19:58:22 2009 +0100
@@ -9,29 +9,9 @@
import scala.actors.Actor, Actor._
-
import scala.collection.mutable
import isabelle.jedit.Isabelle
-import isabelle.XML
-
-
-trait Accumulator extends Actor
-{
- start() // start actor
-
- protected var _state: State
- def state = _state
-
- override def act() {
- loop {
- react {
- case (session: Session, message: XML.Tree) => _state = _state.+(session, message)
- case bad => System.err.println("Accumulator: ignoring bad message " + bad)
- }
- }
- }
-}
object Command
@@ -53,15 +33,14 @@
class Command(
val id: Isar_Document.Command_ID,
val tokens: List[Token],
- val starts: Map[Token, Int]) extends Accumulator with Session.Entity
+ val starts: Map[Token, Int])
+ extends Session.Entity
{
require(!tokens.isEmpty)
// FIXME override equality as well
override def hashCode = id.hashCode
- def consume(session: Session, message: XML.Tree) { this ! (session, message) }
-
/* content */
@@ -77,7 +56,38 @@
def contains(p: Token) = tokens.contains(p)
- protected override var _state = new State(this)
+
+ /* accumulated messages */
+
+ @volatile protected var state = new State(this)
+ def current_state: State = state
+
+ private case class Consume(session: Session, message: XML.Tree)
+ private case object Finish
+
+ private val accumulator = actor {
+ var finished = false
+ loop {
+ react {
+ case Consume(session: Session, message: XML.Tree) if !finished =>
+ state = state.+(session, message)
+
+ case Finish => finished = true; reply(())
+
+ case bad => System.err.println("command accumulator: ignoring bad message " + bad)
+ }
+ }
+ }
+
+ def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
+
+ def finish_static(state_id: Isar_Document.State_ID): Command =
+ {
+ val cmd = new Command(state_id, tokens, starts)
+ accumulator !? Finish
+ cmd.state = current_state
+ cmd
+ }
/* markup */
@@ -92,39 +102,22 @@
}
- /* results, markup, ... */
+ /* results, markup, etc. */
- private val empty_cmd_state = new Command_State("", this) // FIXME ?
- private def cmd_state(doc: Proof_Document) = // FIXME clarify
- doc.states.getOrElse(this, empty_cmd_state)
+ def results: List[XML.Tree] = current_state.results
+ def markup_root: Markup_Text = current_state.markup_root
+ def type_at(pos: Int): Option[String] = current_state.type_at(pos)
+ def ref_at(pos: Int): Option[Markup_Node] = current_state.ref_at(pos)
+ def highlight: Markup_Text = current_state.highlight
- def status(doc: Proof_Document) = cmd_state(doc).state.status
+
+ private def cmd_state(doc: Proof_Document): State = // FIXME clarify
+ doc.states.getOrElse(this, this).current_state
+
+ def status(doc: Proof_Document) = cmd_state(doc).status
def results(doc: Proof_Document) = cmd_state(doc).results
def markup_root(doc: Proof_Document) = cmd_state(doc).markup_root
def highlight(doc: Proof_Document) = cmd_state(doc).highlight
def type_at(doc: Proof_Document, offset: Int) = cmd_state(doc).type_at(offset)
def ref_at(doc: Proof_Document, offset: Int) = cmd_state(doc).ref_at(offset)
}
-
-
-class Command_State(
- override val id: Isar_Document.State_ID,
- val command: Command) extends Accumulator with Session.Entity
-{
- protected override var _state = new State(command)
-
- def consume(session: Session, message: XML.Tree) { this ! (session, message) }
-
- def results: List[XML.Tree] =
- command.state.results ::: state.results
-
- def markup_root: Markup_Text =
- (command.state.markup_root /: state.markup_root.markup)(_ + _)
-
- def type_at(pos: Int): Option[String] = state.type_at(pos)
-
- def ref_at(pos: Int): Option[Markup_Node] = state.ref_at(pos)
-
- def highlight: Markup_Text =
- (command.state.highlight /: state.highlight.markup)(_ + _)
-}
\ No newline at end of file
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala Wed Dec 30 18:22:10 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala Wed Dec 30 19:58:22 2009 +0100
@@ -42,7 +42,7 @@
val tokens: Linear_Set[Token], // FIXME plain List, inside Command
val token_start: Map[Token, Int], // FIXME eliminate
val commands: Linear_Set[Command],
- var states: Map[Command, Command_State]) // FIXME immutable, eliminate!?
+ var states: Map[Command, Command]) // FIXME immutable, eliminate!?
{
import Proof_Document.StructureChange
--- a/src/Tools/jEdit/src/proofdocument/session.scala Wed Dec 30 18:22:10 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Wed Dec 30 19:58:22 2009 +0100
@@ -9,6 +9,7 @@
import scala.actors.Actor._
+
object Session
{
/* events */
@@ -51,11 +52,11 @@
@volatile private var outer_syntax = new Outer_Syntax(system.symbols)
def syntax(): Outer_Syntax = outer_syntax
- @volatile private var states = Map[Isar_Document.State_ID, Command_State]()
+ @volatile private var states = Map[Isar_Document.State_ID, Command]()
@volatile private var commands = Map[Isar_Document.Command_ID, Command]()
@volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
- def state(id: Isar_Document.State_ID): Option[Command_State] = states.get(id)
+ def state(id: Isar_Document.State_ID): Option[Command] = states.get(id)
def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
@@ -124,7 +125,7 @@
{
commands.get(cmd_id) match {
case Some(cmd) =>
- val state = new Command_State(state_id, cmd)
+ val state = cmd.finish_static(state_id)
states += (state_id -> state)
doc.states += (cmd -> state)
command_change.event(cmd) // FIXME really!?