more explicit treatment of command/document state;
misc tuning and clarification;

--- a/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -25,7 +25,7 @@
 {
   def choose_color(command: Command, doc: Document): Color =
   {
-    command.status(doc) match {
+    doc.current_state(command).status match {
       case Command.Status.UNPROCESSED => new Color(255, 228, 225)
       case Command.Status.FINISHED => new Color(234, 248, 255)
       case Command.Status.FAILED => new Color(255, 193, 193)
@@ -132,7 +132,7 @@
       document.command_at(offset) match {
         case Some(cmd) =>
           document.token_start(cmd.tokens.first)
-          cmd.type_at(document, offset - cmd.start(document)).getOrElse(null)
+          document.current_state(cmd).type_at(offset - cmd.start(document)).getOrElse(null)
         case None => null
       }
     }

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -45,7 +45,7 @@
         val offset = model.from_current(document, original_offset)
         document.command_at(offset) match {
           case Some(command) =>
-            command.ref_at(document, offset - command.start(document)) match {
+            document.current_state(command).ref_at(offset - command.start(document)) match {
               case Some(ref) =>
                 val command_start = command.start(document)
                 val begin = model.to_current(document, command_start + ref.start)

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -45,7 +45,7 @@
       case Some(model) =>
         val document = model.recent_document()
         for (command <- document.commands if !stopped) {
-          root.add(command.markup_root(document).swing_tree((node: Markup_Node) =>
+          root.add(document.current_state(command).markup_root.swing_tree((node: Markup_Node) =>
               {
                 val content = command.content(node.start, node.stop)
                 val command_start = command.start(document)

--- a/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_token_marker.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -119,7 +119,7 @@
     while (cmd.isDefined && cmd.get.start(document) < from(stop)) {
       val command = cmd.get
       for {
-        markup <- command.highlight(document).flatten
+        markup <- document.current_state(command).highlight.flatten
         command_start = command.start(document)
         abs_start = to(command_start + markup.start)
         abs_stop = to(command_start + markup.stop)

--- a/src/Tools/jEdit/src/jedit/output_dockable.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/output_dockable.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -40,7 +40,7 @@
             case Some(model) =>
               val body =
                 if (cmd == null) Nil  // FIXME ??
-                else cmd.results(model.recent_document)
+                else model.recent_document.current_state(cmd).results
               html_panel.render(body)
           }
 

--- a/src/Tools/jEdit/src/proofdocument/command.scala	Sun Jan 03 19:53:58 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala	Sun Jan 03 20:50:07 2010 +0100
@@ -33,7 +33,7 @@
 class Command(
     val id: Isar_Document.Command_ID,
     val tokens: List[Token],
-    val starts: Map[Token, Int])
+    val starts: Map[Token, Int])   // FIXME eliminate
   extends Session.Entity
 {
   require(!tokens.isEmpty)
@@ -49,7 +49,7 @@
   val name = tokens.head.content
   val content: String = Token.string_from_tokens(tokens, starts)
   def content(i: Int, j: Int): String = content.substring(i, j)
-  val symbol_index = new Symbol.Index(content)
+  lazy val symbol_index = new Symbol.Index(content)
 
   def start(doc: Document) = doc.token_start(tokens.first)
   def stop(doc: Document) = doc.token_start(tokens.last) + tokens.last.length
@@ -63,16 +63,18 @@
   def current_state: State = state
 
   private case class Consume(session: Session, message: XML.Tree)
-  private case object Finish
+  private case object Assign
 
   private val accumulator = actor {
-    var finished = false
+    var assigned = false
     loop {
       react {
-        case Consume(session: Session, message: XML.Tree) if !finished =>
+        case Consume(session: Session, message: XML.Tree) if !assigned =>
           state = state.+(session, message)
 
-        case Finish => finished = true; reply(())
+        case Assign =>
+          assigned = true  // single assigment
+          reply(())
 
         case bad => System.err.println("command accumulator: ignoring bad message " + bad)
       }
@@ -81,10 +83,10 @@
 
   def consume(session: Session, message: XML.Tree) { accumulator ! Consume(session, message) }
 
-  def finish_static(state_id: Isar_Document.State_ID): Command =
+  def assign_state(state_id: Isar_Document.State_ID): Command =
   {
     val cmd = new Command(state_id, tokens, starts)
-    accumulator !? Finish
+    accumulator !? Assign
     cmd.state = current_state
     cmd
   }
@@ -100,24 +102,4 @@
     val stop = symbol_index.decode(end)
     new Markup_Tree(new Markup_Node(start, stop, info), Nil)
   }
-
-
-  /* results, markup, etc. */
-
-  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
-
-
-  private def cmd_state(doc: Document): State =  // FIXME clarify
-    doc.states.getOrElse(this, this).current_state
-
-  def status(doc: Document) = cmd_state(doc).status
-  def results(doc: Document) = cmd_state(doc).results
-  def markup_root(doc: Document) = cmd_state(doc).markup_root
-  def highlight(doc: Document) = cmd_state(doc).highlight
-  def type_at(doc: Document, offset: Int) = cmd_state(doc).type_at(offset)
-  def ref_at(doc: Document, offset: Int) = cmd_state(doc).ref_at(offset)
 }

--- 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 _ =>
                 }
               }