abs. stops, markup nodes depend on doc-version;
fixed missing positions in ProofDocument.text_changed;
relink only changed commands in ProofDocument.token_changed

--- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -74,22 +74,22 @@
     val start = buffer.getLineStartOffset(line)
     val stop = start + line_segment.count
 
-    val current_document = prover.document
-   
-    def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(current_document.id, _)
-    def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(current_document.id, _)
+    val document = prover.document
+
+    def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(document.id, _)
+    def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
 
     var next_x = start
     for {
-      command <- current_document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
+      command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
       markup <- command.root_node.flatten
-      if(to(markup.abs_stop) > start)
-      if(to(markup.abs_start) < stop)
+      if(to(markup.abs_stop(document)) > start)
+      if(to(markup.abs_start(document)) < stop)
       byte = DynamicTokenMarker.choose_byte(markup.kind)
-      token_start = to(markup.abs_start) - start max 0
-      token_length = to(markup.abs_stop) - to(markup.abs_start) -
-                     (start - to(markup.abs_start) max 0) -
-                     (to(markup.abs_stop) - stop max 0)
+      token_start = to(markup.abs_start(document)) - start max 0
+      token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
+                     (start - to(markup.abs_start(document)) max 0) -
+                     (to(markup.abs_stop(document)) - stop max 0)
     } {
       if (start + token_start > next_x)
         handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)

--- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -33,7 +33,7 @@
     if (prover_setup.isDefined) {
         val document = prover_setup.get.prover.document
         for (command <- document.commands)
-          data.root.add(command.root_node.swing_node)
+          data.root.add(command.root_node.swing_node(document))
         
         if (stopped) data.root.add(new DefaultMutableTreeNode("<parser stopped>"))
     } else {

--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -7,6 +7,7 @@
 package isabelle.jedit
 
 import isabelle.prover.Command
+import isabelle.proofdocument.ProofDocument
 import isabelle.utils.Delay
 
 import javax.swing._
@@ -57,9 +58,9 @@
     } else ""
 	}
 
-  private def paintCommand(command : Command, buffer : JEditBuffer, doc_id: String, gfx : Graphics) {
-    val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start))
-    val line2 = buffer.getLineOfOffset(to_current(doc_id, command.stop - 1)) + 1
+  private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
+    val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc)))
+    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc) - 1)) + 1
     val y = lineToY(line1)
     val height = lineToY(line2) - y - 1
     val (light, dark) = command.status match {
@@ -82,7 +83,7 @@
 		val buffer = textarea.getBuffer
     val document = prover.document
     for (c <- document.commands)
-      paintCommand(c, buffer, document.id, gfx)
+      paintCommand(c, buffer, document, gfx)
 
 	}
 

--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -66,8 +66,9 @@
 
   private val selected_state_controller = new CaretListener {
     override def caretUpdate(e: CaretEvent) = {
-      val cmd = prover.document.find_command_at(e.getDot)
-      if (cmd != null && cmd.start <= e.getDot &&
+      val doc = prover.document
+      val cmd = doc.find_command_at(e.getDot)
+      if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
           Isabelle.prover_setup(buffer).get.selected_state != cmd)
         Isabelle.prover_setup(buffer).get.selected_state = cmd
     }
@@ -141,8 +142,8 @@
   {
     val document = prover.document
     if (text_area != null) {
-      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start))
-      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1)
+      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
+      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
       text_area.invalidateLineRange(start, stop)
 
       if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
@@ -189,18 +190,18 @@
 
     val metrics = text_area.getPainter.getFontMetrics
     var e = document.find_command_at(from_current(start))
-    val commands = document.commands.dropWhile(_.stop <= from_current(start)).
-      takeWhile(c => to_current(c.start) < end)
+    val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
+      takeWhile(c => to_current(c.start(document)) < end)
     // encolor phase
     for (e <- commands) {
-      val begin = start max to_current(e.start)
-      val finish = end - 1 min to_current(e.stop)
+      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)
 
       // paint details of command
       for (node <- e.root_node.dfs) {
-        val begin = to_current(node.start + e.start)
-        val finish = to_current(node.stop + e.start)
+        val begin = to_current(node.abs_start(document))
+        val finish = to_current(node.abs_stop(document))
         if (finish > start && begin < end) {
           encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
             DynamicTokenMarker.choose_color(node.kind, text_area.getPainter.getStyles), true)

--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -75,16 +75,25 @@
     val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed)
     // update indices
     start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed)))
-    start = removed.foldLeft (start) ((s, t) => s - t)
 
     val split_begin = removed.takeWhile(start(_) < change.start).
-      map (t => new Token(t.content.substring(0, change.start - start(t)),
-                          t.kind))
+      map (t => {
+          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
+          start += (split_tok -> start(t))
+          split_tok
+        })
+
     val split_end = removed.dropWhile(stop(_) < change.start + change.removed).
-      map (t => new Token(t.content.substring(change.start + change.removed - start(t)),
-                          t.kind))
+      map (t => {
+          val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)),
+                          t.kind)
+          start += (split_tok -> start(t))
+          split_tok
+        })
     // update indices
-    start = split_end.foldLeft (start) ((s, t) => s + (t -> (change.start + change.added.length)))
+    start = removed.foldLeft (start) ((s, t) => s - t)
+    start = split_end.foldLeft (start) ((s, t) =>
+    s + (t -> (change.start + change.added.length)))
 
     val ins = new Token(change.added, Token.Kind.OTHER)
     start += (ins -> change.start)
@@ -121,77 +130,75 @@
     }
     val insert = new_tokens.reverse
     val new_token_list = begin ::: insert ::: old_suffix
+    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
     token_changed(change.id,
                   begin.lastOption,
                   insert,
-                  removed,
                   old_suffix.firstOption,
-                  new_token_list,
+                  new_tokenset,
                   start)
   }
   
   /** command view **/
 
   def find_command_at(pos: Int): Command = {
-    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
+    for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
     return null
   }
 
   private def token_changed(new_id: String,
                             before_change: Option[Token],
                             inserted_tokens: List[Token],
-                            removed_tokens: List[Token],
                             after_change: Option[Token],
-                            new_token_list: List[Token],
+                            new_tokenset: LinearSet[Token],
                             new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
   {
-    val commands_list = List[Command]() ++ commands
-
-    // calculate removed commands
-    val first_removed = removed_tokens.firstOption
+    val cmd_first_changed =
+      if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
+      else None
+    val cmd_last_changed =
+      if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
+      else None
 
-    val (begin, remaining) =
-      first_removed match {
-        case None => (Nil, commands_list)
-        case Some(fr) => commands_list.break(_.tokens.contains(fr))
-      }
-    val (removed_commands, end) =
-      after_change match {
-        case None => (remaining, Nil)
-        case Some(ac) => remaining.break(_.tokens.contains(ac))
-      }
+    val cmd_before_change =
+      if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
+      else None
+    val cmd_after_change =
+      if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
+      else None
 
+    val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
+      takeWhile(Some(_) != cmd_after_change)
+
+    // calculate inserted commands
     def tokens_to_commands(tokens: List[Token]): List[Command]= {
       tokens match {
         case Nil => Nil
         case t::ts =>
           val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
-          new Command(t::cmd) :: tokens_to_commands (rest)
+          new Command(t::cmd, new_token_start) :: tokens_to_commands (rest)
       }
     }
 
-    // calculate inserted commands
-    val new_commands = tokens_to_commands(new_token_list)
-    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
-    val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]]
-    // drop known commands from the beginning
-    val first_changed = before_change match {
-      case None => new_tokenset.first_elem
-      case Some(bc) => new_tokenset.next(bc)
-    }
-    val changed_commands = first_changed match {
-      case None => Nil
-      case Some(fc) => new_commands.dropWhile(!_.tokens.contains(fc))
-    }
-    val inserted_commands = after_change match {
-      case None => changed_commands
-      case Some(ac) => changed_commands.takeWhile(!_.tokens.contains(ac))
-    }
-    val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)),
-                                     inserted_commands, removed_commands)
+    val split_begin_tokens =
+      if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
+      else {
+        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
+      }
+    val split_end_tokens =
+      if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
+      else {
+        cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
+      }
+
+    val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
+    val inserted_commands = tokens_to_commands(rescanning_tokens)
+
+    val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
     // build new document
-    var new_commands = commands
-    while(new_commands.next())
+    val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change).
+        insert_after(cmd_before_change, inserted_commands)
+
     val doc =
       new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
     return (doc, change)

--- a/src/Tools/jEdit/src/proofdocument/Token.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -38,5 +38,5 @@
 
 class Token(val content: String, val kind: Token.Kind.Value) {
   val length = content.length
-  override def toString = content + "(" + kind + ")"
+  override def toString = content
 }

--- a/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Command.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -29,7 +29,7 @@
 }
 
 
-class Command(val tokens: List[Token])
+class Command(val tokens: List[Token], val starts: Map[Token, Int])
 {
   val id = Isabelle.plugin.id()
 
@@ -38,10 +38,10 @@
   override def toString = name
 
   val name = tokens.head.content
-  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
+  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), starts)
 
-  def start = tokens.first.start
-  def stop = tokens.last.stop
+  def start(doc: ProofDocument) = doc.token_start(tokens.first)
+  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
 
   /* command status */
 
@@ -80,10 +80,14 @@
   /* markup */
 
   val root_node =
-    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
+    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content)
 
-  def node_from(kind: String, begin: Int, end: Int) = {
-    val markup_content = content.substring(begin, end)
-    new MarkupNode(this, begin, end, id, kind, markup_content)
+  def add_markup(kind: String, begin: Int, end: Int) = {
+    val markup_content = if (end <= content.length) content.substring(begin, end)
+      else {
+        System.err.println (root_node.stop, content, content.length, end)
+        "wrong indices?"
+      }
+    root_node insert new MarkupNode(this, begin, end, id, kind, markup_content)
   }
 }

--- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -6,6 +6,8 @@
 
 package isabelle.prover
 
+import isabelle.proofdocument.ProofDocument
+
 import sidekick.IAsset
 import javax.swing._
 import javax.swing.text.Position
@@ -13,10 +15,10 @@
 
 object MarkupNode {
 
-  def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = {
+  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
 
     implicit def int2pos(offset: Int): Position =
-      new Position { def getOffset = offset }
+      new Position { def getOffset = offset; override def toString = offset.toString}
 
     object RelativeAsset extends IAsset {
       override def getIcon : Icon = null
@@ -25,10 +27,10 @@
       override def getName : String = node.id
       override def setName (name : String) = ()
       override def setStart(start : Position) = ()
-      override def getStart : Position = node.abs_start
+      override def getStart : Position = node.abs_start(doc)
       override def setEnd(end : Position) = ()
-      override def getEnd : Position = node.abs_stop
-      override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]"
+      override def getEnd : Position = node.abs_stop(doc)
+      override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]"
     }
 
     new DefaultMutableTreeNode(RelativeAsset)
@@ -38,40 +40,27 @@
 class MarkupNode (val base : Command, val start : Int, val stop : Int,
                     val id : String, val kind : String, val desc : String) {
 
-  val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
+  def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
+    val node = MarkupNode.markup2default_node (this, base, doc)
+    for (c <- children) node add c.swing_node(doc)
+    node
+  }
+    
+  def abs_start(doc: ProofDocument) = base.start(doc) + start
+  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
 
   var parent : MarkupNode = null
   def orphan = parent == null
 
-  def length = stop - start
-  def abs_start = base.start + start
-  def abs_stop = base.start + stop
-
-  private var children_cell : List[MarkupNode] = Nil
-  //track changes in swing_node
-  def children = children_cell
-  def children_= (cs : List[MarkupNode]) = {
-    swing_node.removeAllChildren
-    for (c <- cs) swing_node add c.swing_node
-    children_cell = cs
-  }
+  var children : List[MarkupNode] = Nil
 
   private def add(child : MarkupNode) {
     child parent = this
-    children_cell = (child :: children) sort ((a, b) => a.start < b.start)
-
-    swing_node add child.swing_node
+    children = (child :: children) sort ((a, b) => a.start < b.start)
   }
 
   private def remove(nodes : List[MarkupNode]) {
-    children_cell = children diff nodes
-
-      for (node <- nodes) try {
-        swing_node remove node.swing_node
-      } catch { case e : IllegalArgumentException =>
-        System.err.println(e.toString)
-        case e => throw e
-      }
+    children = children diff nodes
   }
 
   def dfs : List[MarkupNode] = {

--- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -190,7 +190,7 @@
                       // inner syntax: id from props
                       else command
                     if (cmd != null) {
-                      cmd.root_node.insert(cmd.node_from(kind, begin, end))
+                      cmd.add_markup(kind, begin, end)
                       command_change(cmd)
                     }
                   case _ =>
@@ -249,7 +249,7 @@
       for (cmd <- changes.removed_commands) yield {
         commands -= cmd.id
         if (cmd.state_id != null) states -= cmd.state_id
-        (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None
+        changes.before_change.map(_.id).getOrElse(document_id0) -> None
       }
     val inserts =
       for (cmd <- changes.added_commands) yield {

--- a/src/Tools/jEdit/src/utils/LinearSet.scala	Mon Apr 20 20:28:45 2009 +0200
+++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Wed Apr 22 17:35:49 2009 +0200
@@ -43,7 +43,7 @@
   def contains(elem: A): Boolean =
     !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
 
-  def insert_after(hook: Option[A], elem: A): LinearSet[A] =
+  private def _insert_after(hook: Option[A], elem: A): LinearSet[A] =
     if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
     else hook match {
       case Some(hook) =>
@@ -55,8 +55,11 @@
         if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
         else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
     }
-    
-  def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
+
+  def insert_after(hook: Option[A], elems: Seq[A]): LinearSet[A] =
+    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
+
+  def +(elem: A): LinearSet[A] = _insert_after(last_elem, elem)
 
   def delete_after(elem: Option[A]): LinearSet[A] =
     elem match {
@@ -70,7 +73,18 @@
         else if (size == 1) empty
         else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
     }
-    
+
+  def delete_between(from: Option[A], to: Option[A]): LinearSet[A] = {
+    if(!first_elem.isDefined) this
+    else {
+      val next = if (from == last_elem) None
+                 else if (from == None) first_elem
+                 else from.map(body(_))
+      if (next == to) this
+      else delete_after(from).delete_between(from, to)
+    }
+  }
+
   def -(elem: A): LinearSet[A] =
     if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
     else delete_after(body find (p => p._2 == elem) map (p => p._1))