# HG changeset patch
# User wenzelm
# Date 1262199502 -3600
# Node ID 6bae73cd8e33b31e8f709c9efb5cd10edaec4af1
# Parent  0b788ea1ceac68a4418caa8bf6a6649da1d62ee0
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);

diff -r 0b788ea1ceac -r 6bae73cd8e33 src/Tools/jEdit/src/proofdocument/command.scala
--- 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
diff -r 0b788ea1ceac -r 6bae73cd8e33 src/Tools/jEdit/src/proofdocument/proof_document.scala
--- 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
 
diff -r 0b788ea1ceac -r 6bae73cd8e33 src/Tools/jEdit/src/proofdocument/session.scala
--- 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!?