--- a/src/Tools/jEdit/src/proofdocument/document.scala Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala Sun Jan 03 20:50:07 2010 +0100
@@ -60,7 +60,7 @@
val tokens: Linear_Set[Token], // FIXME plain List, inside Command
val token_start: Map[Token, Int], // FIXME eliminate
val commands: Linear_Set[Command],
- @volatile var states: Map[Command, Command]) // FIXME immutable, eliminate!?
+ old_states: Map[Command, Command])
extends Session.Entity
{
def content = Token.string_from_tokens(Nil ++ tokens, token_start)
@@ -68,6 +68,11 @@
/* accumulated messages */
+ @volatile private var states = old_states
+
+ def current_state(cmd: Command): State =
+ states.getOrElse(cmd, cmd).current_state
+
private val accumulator = actor {
loop {
react {
@@ -80,10 +85,9 @@
} {
session.lookup_entity(cmd_id) match {
case Some(cmd: Command) =>
- val state = cmd.finish_static(state_id) // FIXME more explicit typing
+ val state = cmd.assign_state(state_id)
session.register_entity(state)
- states += (cmd -> state) // FIXME !?
- session.command_change.event(cmd) // FIXME really!?
+ states += (cmd -> state)
case _ =>
}
}