src/Tools/jEdit/src/prover/Command.scala

--- a/src/Tools/jEdit/src/prover/Command.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -36,7 +36,7 @@
   require(!tokens.isEmpty)
 
   val id = Isabelle.system.id()
-
+  override def hashCode = id.hashCode
 
   /* content */
 
@@ -51,40 +51,42 @@
 
   def contains(p: Token) = tokens.contains(p)
 
-
-  /* command status */   // FIXME class Command_State, multiple states per command
-
-  var state_id: IsarDocument.State_ID = null
+  /* states */
+  val states = mutable.Map[IsarDocument.State_ID, Command_State]()
+  private def state(doc: ProofDocument) = doc.states.get(this)
+  
+  /* command status */
 
-  private var _status = Command.Status.UNPROCESSED
-  def status = _status
-  def status_=(st: Command.Status.Value) {
-    if (st == Command.Status.UNPROCESSED) {
-      state_results.clear
-      // delete markup
-      markup_root = markup_root.filter(_.info match {
-          case RootInfo() | OuterInfo(_) => true
-          case _ => false
-        }).head
-    }
-    _status = st
+  def set_status(state: IsarDocument.State_ID, status: Command.Status.Value) = {
+    if (state != null)
+      states.getOrElseUpdate(state, new Command_State(this)).status = status
   }
 
+  def status(doc: ProofDocument) =
+    state(doc) match {
+      case Some(s) => states.getOrElseUpdate(s, new Command_State(this)).status
+      case _ => Command.Status.UNPROCESSED
+    }
 
   /* results */
 
   private val results = new mutable.ListBuffer[XML.Tree]
-  private val state_results = new mutable.ListBuffer[XML.Tree]
-  def add_result(running: Boolean, tree: XML.Tree) = synchronized {
-    (if (running) state_results else results) += tree
+  def add_result(state: IsarDocument.State_ID, tree: XML.Tree) = synchronized {
+    (if (state == null) results else states(state).results) += tree
   }
 
-  def result_document = XML.document(
-    results.toList ::: state_results.toList match {
-      case Nil => XML.Elem("message", Nil, Nil)
-      case List(elem) => elem
-      case elems => XML.Elem("messages", Nil, elems)
-    }, "style")
+  def result_document(doc: ProofDocument) = {
+    val state_results = state(doc) match {
+      case Some(s) =>
+        states.getOrElseUpdate(s, new Command_State(this)).results
+      case _ => Nil}
+    XML.document(
+      results.toList ::: state_results.toList match {
+        case Nil => XML.Elem("message", Nil, Nil)
+        case List(elem) => elem
+        case elems => XML.Elem("messages", Nil, elems)
+      }, "style")
+  }
 
 
   /* markup */
@@ -92,13 +94,27 @@
   val empty_root_node =
     new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length,
       Nil, id, content, RootInfo())
+  private var _markup_root = empty_root_node
+  def add_markup(state: IsarDocument.State_ID, node: MarkupNode) = {
+    if (state == null) _markup_root = _markup_root.add(node)
+    else {
+      val cmd_state = states.getOrElseUpdate(state, new Command_State(this))
+      cmd_state.markup_root += node
+    }
+  }
 
-  var markup_root = empty_root_node
+  def markup_root(doc: ProofDocument): MarkupNode = {
+    state(doc) match {
+      case Some(s) =>
+        (_markup_root /: states(s).markup_root.children) (_ + _)
+      case _ => _markup_root
+    }
+  }
 
-  def highlight_node: MarkupNode =
+  def highlight_node(doc: ProofDocument): MarkupNode =
   {
     import MarkupNode._
-    markup_root.filter(_.info match {
+    markup_root(doc).filter(_.info match {
       case RootInfo() | OuterInfo(_) | HighlightInfo(_) => true
       case _ => false
     }).head
@@ -110,6 +126,25 @@
       else "wrong indices??",
       info)
 
+  def type_at(doc: ProofDocument, pos: Int) =
+    state(doc).map(states(_).type_at(pos)).getOrElse(null)
+
+  def ref_at(doc: ProofDocument, pos: Int) =
+    state(doc).flatMap(states(_).ref_at(pos))
+
+}
+
+class Command_State(val cmd: Command) {
+
+  var status = Command.Status.UNPROCESSED
+
+  /* results */
+  val results = new mutable.ListBuffer[XML.Tree]
+
+  /* markup */
+  val empty_root_node = cmd.empty_root_node
+  var markup_root = empty_root_node
+
   def type_at(pos: Int): String =
   {
     val types = markup_root.filter(_.info match { case TypeInfo(_) => true case _ => false })