# HG changeset patch
# User immler@in.tum.de
# Date 1247058915 -7200
# Node ID 2e033aaf128ef130bf19cbfc332d8c39804a5f9c
# Parent  5fe5e00ec430b73afc3d70595e96c706318c5df9
commands carrying state-information

diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala
--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -115,7 +115,7 @@
     var next_x = start
     while (command != null && command.start(document) < from(stop)) {
       for {
-        markup <- command.highlight_node.flatten
+        markup <- command.highlight_node(document).flatten
         if (to(markup.abs_stop(document)) > start)
         if (to(markup.abs_start(document)) < stop)
         byte = DynamicTokenMarker.choose_byte(markup.info.toString)
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleHyperlinkSource.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -52,8 +52,9 @@
       val document = theory_view.current_document()
       val offset = theory_view.from_current(document, original_offset)
       val cmd = document.find_command_at(offset)
+      val state = document.states(cmd)
       if (cmd != null) {
-        val ref_o = cmd.ref_at(offset - cmd.start(document))
+        val ref_o = cmd.ref_at(document, offset - cmd.start(document))
         if (!ref_o.isDefined) null
         else {
           val ref = ref_o.get
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala
--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -34,7 +34,7 @@
     if (prover_setup.isDefined) {
       val document = prover_setup.get.theory_view.current_document()
       for (command <- document.commands)
-        data.root.add(command.markup_root.swing_node(document))
+        data.root.add(command.markup_root(document).swing_node(document))
 
       if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     }
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -63,7 +63,7 @@
     val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc))) + 1
     val y = lineToY(line1)
     val height = lineToY(line2) - y - 1
-    val (light, dark) = command.status match {
+    val (light, dark) = command.status(doc) match {
       case Command.Status.UNPROCESSED => (Color.yellow, new Color(128,128,0))
       case Command.Status.FINISHED => (Color.green, new Color(0, 128, 0))
       case Command.Status.FAILED => (Color.red, new Color(128,0,0))
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -58,16 +58,17 @@
       })
 
     // register for state-view
-    state_update += (state => {
+    state_update += (cmd => {
       val state_view = view.getDockableWindowManager.getDockable("isabelle-state")
       val state_panel =
         if (state_view != null) state_view.asInstanceOf[StateViewDockable].panel
         else null
       if (state_panel != null) {
-        if (state == null)
+        if (cmd == null)
           state_panel.setDocument(null: Document)
         else
-          state_panel.setDocument(state.result_document, UserAgent.base_URL)
+          state_panel.setDocument(cmd.result_document(theory_view.current_document()),
+            UserAgent.base_URL)
       }
     })
 
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -11,7 +11,7 @@
 import scala.actors.Actor
 import scala.actors.Actor._
 
-import isabelle.proofdocument.Text
+import isabelle.proofdocument.{ProofDocument, Text}
 import isabelle.prover.{Prover, ProverEvents, Command}
 
 import java.awt.Graphics2D
@@ -30,15 +30,13 @@
 
   val MAX_CHANGE_LENGTH = 1500
   
-  def choose_color(state: Command): Color = {
-    if (state == null) Color.red
-    else
-      state.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, 192, 192)
-        case _ => Color.red
-      }
+  def choose_color(cmd: Command, doc: ProofDocument): Color = {
+    cmd.status(doc) 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, 192, 192)
+      case _ => Color.red
+    }
   }
 }
 
@@ -176,8 +174,11 @@
 
     val content = buffer.getText(0, buffer.getLength)
     doc_id = id
-    /* listen for changes again (TODO: can it be that Listener gets events that
-      happenend prior to registration??) */
+    // invoke repaint
+    update_delay()
+    repaint_delay()
+    phase_overview.repaint_delay()
+
     buffer.addBufferListener(this)
   }
 
@@ -238,7 +239,8 @@
     while (e != null && e.start(document) < end) {
       val begin = start max to_current(e.start(document))
       val finish = end - 1 min to_current(e.stop(document))
-      encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
+      encolor(gfx, y, metrics.getHeight, begin, finish,
+        TheoryView.choose_color(e, document), true)
       e = document.commands.next(e).getOrElse(null)
     }
 
@@ -251,7 +253,7 @@
     val cmd = document.find_command_at(offset)
     if (cmd != null) {
       document.token_start(cmd.tokens.first)
-      cmd.type_at(offset - cmd.start(document))
+      cmd.type_at(document, offset - cmd.start(document))
     } else null
   }
 
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -40,7 +40,7 @@
 
  val empty =
   new ProofDocument(isabelle.jedit.Isabelle.system.id(),
-    LinearSet(), Map(), LinearSet(), _ => false)
+    LinearSet(), Map(), LinearSet(), Map(), _ => false)
 
 }
 
@@ -49,11 +49,13 @@
   val tokens: LinearSet[Token],
   val token_start: Map[Token, Int],
   val commands: LinearSet[Command],
+  var states: Map[Command, IsarDocument.State_ID],
   is_command_keyword: String => Boolean)
 {
 
+
   def set_command_keyword(f: String => Boolean): ProofDocument =
-    new ProofDocument(id, tokens, token_start, commands, f)
+    new ProofDocument(id, tokens, token_start, commands, states, f)
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
   /** token view **/
@@ -214,7 +216,7 @@
 
     val doc =
       new ProofDocument(new_id, new_tokenset, new_token_start,
-        new_commandset, is_command_keyword)
+        new_commandset, states -- removed_commands, is_command_keyword)
     return (doc, change)
   }
 
diff -r 5fe5e00ec430 -r 2e033aaf128e 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 })
diff -r 5fe5e00ec430 -r 2e033aaf128e src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 15:15:13 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Jul 08 15:15:15 2009 +0200
@@ -91,13 +91,13 @@
   private def handle_result(result: Isabelle_Process.Result)
   {
     def command_change(c: Command) = change_receiver ! c
-    val (running, command) =
+    val (state, command) =
       result.props.find(p => p._1 == Markup.ID) match {
-        case None => (false, null)
+        case None => (null, null)
         case Some((_, id)) =>
-          if (commands.contains(id)) (false, commands(id))
-          else if (states.contains(id)) (true, states(id))
-          else (false, null)
+          if (commands.contains(id)) (null, commands(id))
+          else if (states.contains(id)) (id, states(id))
+          else (null, null)
       }
 
     if (result.kind == Isabelle_Process.Kind.STDOUT ||
@@ -112,8 +112,8 @@
         | Isabelle_Process.Kind.ERROR =>
           if (command != null) {
             if (result.kind == Isabelle_Process.Kind.ERROR)
-              command.status = Command.Status.FAILED
-            command.add_result(running, process.parse_message(result))
+              command.set_status(state, Command.Status.FAILED)
+            command.add_result(state, process.parse_message(result))
             command_change(command)
           } else {
             output_info.event(result.toString)
@@ -143,16 +143,16 @@
                   case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits)
                   if document_versions.exists(_.id == doc_id) =>
                     output_info.event(result.toString)
+                    val doc = document_versions.find(_.id == doc_id).get
                     for {
                       XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
                         <- edits
                     } {
                       if (commands.contains(cmd_id)) {
                         val cmd = commands(cmd_id)
-                        if (cmd.state_id != null) states -= cmd.state_id
                         states(state_id) = cmd
-                        cmd.state_id = state_id
-                        cmd.status = Command.Status.UNPROCESSED
+                        doc.states += (cmd -> state_id)
+                        cmd.states += (state_id -> new Command_State(cmd))
                         command_change(cmd)
                       }
 
@@ -161,17 +161,17 @@
                   case XML.Elem(Markup.UNPROCESSED, _, _)
                   if command != null =>
                     output_info.event(result.toString)
-                    command.status = Command.Status.UNPROCESSED
+                    command.set_status(state, Command.Status.UNPROCESSED)
                     command_change(command)
                   case XML.Elem(Markup.FINISHED, _, _)
                   if command != null =>
                     output_info.event(result.toString)
-                    command.status = Command.Status.FINISHED
+                    command.set_status(state, Command.Status.FINISHED)
                     command_change(command)
                   case XML.Elem(Markup.FAILED, _, _)
                   if command != null =>
                     output_info.event(result.toString)
-                    command.status = Command.Status.FAILED
+                    command.set_status(state, Command.Status.FAILED)
                     command_change(command)
                   case XML.Elem(kind, attr, body)
                   if command != null =>
@@ -179,23 +179,23 @@
                     if (begin.isDefined && end.isDefined) {
                       if (kind == Markup.ML_TYPING) {
                         val info = body.first.asInstanceOf[XML.Text].content
-                        command.markup_root +=
-                          command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info))
+                        command.add_markup(state,
+                          command.markup_node(begin.get - 1, end.get - 1, TypeInfo(info)))
                       } else if (kind == Markup.ML_REF) {
                         body match {
                           case List(XML.Elem(Markup.ML_DEF, attr, _)) =>
-                            command.markup_root += command.markup_node(
+                            command.add_markup(state, command.markup_node(
                               begin.get - 1, end.get - 1,
                               RefInfo(
                                 Position.file_of(attr),
                                 Position.line_of(attr),
                                 Position.id_of(attr),
-                                Position.offset_of(attr)))
+                                Position.offset_of(attr))))
                           case _ =>
                         }
                       } else {
-                        command.markup_root +=
-                          command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind))
+                        command.add_markup(state,
+                          command.markup_node(begin.get - 1, end.get - 1, HighlightInfo(kind)))
                       }
                     }
                     command_change(command)
@@ -206,10 +206,10 @@
                     val (begin, end) = Position.offsets_of(attr)
                     val markup_id = Position.id_of(attr)
                     val outer = isabelle.jedit.DynamicTokenMarker.is_outer(kind)
-                    if (outer && !running && begin.isDefined && end.isDefined && markup_id.isDefined)
+                    if (outer && state == null && begin.isDefined && end.isDefined && markup_id.isDefined)
                       commands.get(markup_id.get).map (cmd => {
-                        cmd.markup_root +=
-                          cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind))
+                        cmd.add_markup(state,
+                          cmd.markup_node(begin.get - 1, end.get - 1, OuterInfo(kind)))
                         command_change(cmd)
                       })
                   case _ =>
@@ -249,7 +249,6 @@
     val removes =
       for (cmd <- changes.removed_commands) yield {
         commands -= cmd.id
-        if (cmd.state_id != null) states -= cmd.state_id
         changes.before_change.map(_.id).getOrElse(document_0.id) -> None
       }
     val inserts =