1.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Mar 05 10:53:47 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Thu Mar 05 16:40:49 2009 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  import scala.collection.mutable.ListBuffer
     1.5  import java.util.regex.Pattern
     1.6  import isabelle.prover.{Prover, Command}
     1.7 -
     1.8 +import isabelle.utils.LinearSet
     1.9  
    1.10  case class StructureChange(
    1.11    val before_change: Option[Command],
    1.12 @@ -49,16 +49,17 @@
    1.13  
    1.14    text.changes += (change => text_changed(change))
    1.15  
    1.16 -  var tokens = Nil : List[Token]
    1.17 -  var commands = Nil : List[Command]
    1.18 -  def content = Token.string_from_tokens(tokens)
    1.19 +  var tokens = LinearSet.empty[Token]
    1.20 +  var commands = LinearSet.empty[Command]
    1.21 +  def content = Token.string_from_tokens(List() ++ tokens)
    1.22    /** token view **/
    1.23  
    1.24    private def text_changed(change: Text.Change)
    1.25    {
    1.26 +    val tokens = List() ++ this.tokens
    1.27      val (begin, remaining) = tokens.span(_.stop < change.start)
    1.28 -    val (removed, end) = remaining.span(_.start <= change.start + change.removed)
    1.29 -    for (t <- end) t.start += (change.added.length - change.removed)
    1.30 +    val (removed, end_unshifted) = remaining.span(_.start <= change.start + change.removed)
    1.31 +    val end = for (t <- end_unshifted) yield t.shift(change.added.length - change.removed)
    1.32  
    1.33      val split_begin = removed.takeWhile(_.start < change.start).
    1.34        map (t => new Token(t.start,
    1.35 @@ -99,7 +100,7 @@
    1.36        }
    1.37      }
    1.38      val insert = new_tokens.reverse
    1.39 -    tokens = begin ::: insert ::: old_suffix
    1.40 +    this.tokens = (new LinearSet() ++ (begin ::: insert ::: old_suffix)).asInstanceOf[LinearSet[Token]]
    1.41  
    1.42      token_changed(begin.lastOption,
    1.43                    insert,
    1.44 @@ -121,6 +122,7 @@
    1.45                              removed_tokens: List[Token],
    1.46                              after_change: Option[Token])
    1.47    {
    1.48 +    val commands = List() ++ this.commands
    1.49      val (begin, remaining) =
    1.50        before_change match {
    1.51          case None => (Nil, commands)
    1.52 @@ -162,12 +164,8 @@
    1.53      val new_commands = tokens_to_commands(pseudo_new_pre ::: inserted_tokens ::: pseudo_new_post)
    1.54      System.err.println("new_commands: " + new_commands)
    1.55  
    1.56 -    commands = begin ::: new_commands ::: end
    1.57 +    this.commands = (LinearSet() ++ (begin ::: new_commands ::: end)).asInstanceOf[LinearSet[Command]]
    1.58      val before = begin match {case Nil => None case _ => Some (begin.last)}
    1.59      structural_changes.event(new StructureChange(before, new_commands, removed))
    1.60 -/*
    1.61 -    val old = commands
    1.62 -    commands = tokens_to_commands(tokens)
    1.63 -    structural_changes.event(new StructureChange(None, commands, old)) */
    1.64    }
    1.65  }

     2.1 --- a/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Mar 05 10:53:47 2009 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/Token.scala	Thu Mar 05 16:40:49 2009 +0100
     2.3 @@ -38,8 +38,9 @@
     2.4  
     2.5  }
     2.6  
     2.7 -class Token(var start: Int, val content: String, val kind: Token.Kind.Value) {
     2.8 +class Token(val start: Int, val content: String, val kind: Token.Kind.Value) {
     2.9    val length = content.length
    2.10 -  def stop = start + length
    2.11 +  val stop = start + length
    2.12    override def toString = content + "(" + kind + ")"
    2.13 +  def shift(i: Int) = new Token(start + i, content, kind)
    2.14  }

     3.1 --- a/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 05 10:53:47 2009 +0100
     3.2 +++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Thu Mar 05 16:40:49 2009 +0100
     3.3 @@ -3,6 +3,7 @@
     3.4  
     3.5  Sets with canonical linear order, or immutable linked-lists.
     3.6  */
     3.7 +package isabelle.utils
     3.8  
     3.9  object LinearSet
    3.10  {
    3.11 @@ -32,6 +33,8 @@
    3.12  
    3.13    /* basic methods */
    3.14  
    3.15 +  def next(elem: A) = body.get(elem)
    3.16 +  
    3.17    override def isEmpty: Boolean = !last_elem.isDefined
    3.18    def size: Int = if (isEmpty) 0 else body.size + 1
    3.19