1.1 --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 20 20:28:45 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Wed Apr 22 17:35:49 2009 +0200
     1.3 @@ -74,22 +74,22 @@
     1.4      val start = buffer.getLineStartOffset(line)
     1.5      val stop = start + line_segment.count
     1.6  
     1.7 -    val current_document = prover.document
     1.8 -   
     1.9 -    def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(current_document.id, _)
    1.10 -    def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(current_document.id, _)
    1.11 +    val document = prover.document
    1.12 +
    1.13 +    def to: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.to_current(document.id, _)
    1.14 +    def from: Int => Int = Isabelle.prover_setup(buffer).get.theory_view.from_current(document.id, _)
    1.15  
    1.16      var next_x = start
    1.17      for {
    1.18 -      command <- current_document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
    1.19 +      command <- document.commands.dropWhile(_.stop(document) <= from(start)).takeWhile(_.start(document) < from(stop))
    1.20        markup <- command.root_node.flatten
    1.21 -      if(to(markup.abs_stop) > start)
    1.22 -      if(to(markup.abs_start) < stop)
    1.23 +      if(to(markup.abs_stop(document)) > start)
    1.24 +      if(to(markup.abs_start(document)) < stop)
    1.25        byte = DynamicTokenMarker.choose_byte(markup.kind)
    1.26 -      token_start = to(markup.abs_start) - start max 0
    1.27 -      token_length = to(markup.abs_stop) - to(markup.abs_start) -
    1.28 -                     (start - to(markup.abs_start) max 0) -
    1.29 -                     (to(markup.abs_stop) - stop max 0)
    1.30 +      token_start = to(markup.abs_start(document)) - start max 0
    1.31 +      token_length = to(markup.abs_stop(document)) - to(markup.abs_start(document)) -
    1.32 +                     (start - to(markup.abs_start(document)) max 0) -
    1.33 +                     (to(markup.abs_stop(document)) - stop max 0)
    1.34      } {
    1.35        if (start + token_start > next_x)
    1.36          handler.handleToken(line_segment, 1, next_x - start, start + token_start - next_x, context)

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

     3.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Apr 20 20:28:45 2009 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Apr 22 17:35:49 2009 +0200
     3.3 @@ -7,6 +7,7 @@
     3.4  package isabelle.jedit
     3.5  
     3.6  import isabelle.prover.Command
     3.7 +import isabelle.proofdocument.ProofDocument
     3.8  import isabelle.utils.Delay
     3.9  
    3.10  import javax.swing._
    3.11 @@ -57,9 +58,9 @@
    3.12      } else ""
    3.13  	}
    3.14  
    3.15 -  private def paintCommand(command : Command, buffer : JEditBuffer, doc_id: String, gfx : Graphics) {
    3.16 -    val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start))
    3.17 -    val line2 = buffer.getLineOfOffset(to_current(doc_id, command.stop - 1)) + 1
    3.18 +  private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) {
    3.19 +    val line1 = buffer.getLineOfOffset(to_current(doc.id, command.start(doc)))
    3.20 +    val line2 = buffer.getLineOfOffset(to_current(doc.id, command.stop(doc) - 1)) + 1
    3.21      val y = lineToY(line1)
    3.22      val height = lineToY(line2) - y - 1
    3.23      val (light, dark) = command.status match {
    3.24 @@ -82,7 +83,7 @@
    3.25  		val buffer = textarea.getBuffer
    3.26      val document = prover.document
    3.27      for (c <- document.commands)
    3.28 -      paintCommand(c, buffer, document.id, gfx)
    3.29 +      paintCommand(c, buffer, document, gfx)
    3.30  
    3.31  	}
    3.32  

     4.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 20 20:28:45 2009 +0200
     4.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Wed Apr 22 17:35:49 2009 +0200
     4.3 @@ -66,8 +66,9 @@
     4.4  
     4.5    private val selected_state_controller = new CaretListener {
     4.6      override def caretUpdate(e: CaretEvent) = {
     4.7 -      val cmd = prover.document.find_command_at(e.getDot)
     4.8 -      if (cmd != null && cmd.start <= e.getDot &&
     4.9 +      val doc = prover.document
    4.10 +      val cmd = doc.find_command_at(e.getDot)
    4.11 +      if (cmd != null && doc.token_start(cmd.tokens.first) <= e.getDot &&
    4.12            Isabelle.prover_setup(buffer).get.selected_state != cmd)
    4.13          Isabelle.prover_setup(buffer).get.selected_state = cmd
    4.14      }
    4.15 @@ -141,8 +142,8 @@
    4.16    {
    4.17      val document = prover.document
    4.18      if (text_area != null) {
    4.19 -      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start))
    4.20 -      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1)
    4.21 +      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start(document)))
    4.22 +      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop(document)) - 1)
    4.23        text_area.invalidateLineRange(start, stop)
    4.24  
    4.25        if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
    4.26 @@ -189,18 +190,18 @@
    4.27  
    4.28      val metrics = text_area.getPainter.getFontMetrics
    4.29      var e = document.find_command_at(from_current(start))
    4.30 -    val commands = document.commands.dropWhile(_.stop <= from_current(start)).
    4.31 -      takeWhile(c => to_current(c.start) < end)
    4.32 +    val commands = document.commands.dropWhile(_.stop(document) <= from_current(start)).
    4.33 +      takeWhile(c => to_current(c.start(document)) < end)
    4.34      // encolor phase
    4.35      for (e <- commands) {
    4.36 -      val begin = start max to_current(e.start)
    4.37 -      val finish = end - 1 min to_current(e.stop)
    4.38 +      val begin = start max to_current(e.start(document))
    4.39 +      val finish = end - 1 min to_current(e.stop(document))
    4.40        encolor(gfx, y, metrics.getHeight, begin, finish, TheoryView.choose_color(e), true)
    4.41  
    4.42        // paint details of command
    4.43        for (node <- e.root_node.dfs) {
    4.44 -        val begin = to_current(node.start + e.start)
    4.45 -        val finish = to_current(node.stop + e.start)
    4.46 +        val begin = to_current(node.abs_start(document))
    4.47 +        val finish = to_current(node.abs_stop(document))
    4.48          if (finish > start && begin < end) {
    4.49            encolor(gfx, y + metrics.getHeight - 2, 1, begin max start, finish min end - 1,
    4.50              DynamicTokenMarker.choose_color(node.kind, text_area.getPainter.getStyles), true)

     5.1 --- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Mon Apr 20 20:28:45 2009 +0200
     5.2 +++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala	Wed Apr 22 17:35:49 2009 +0200
     5.3 @@ -75,16 +75,25 @@
     5.4      val (removed, end) = remaining.span(token_start(_) <= change.start + change.removed)
     5.5      // update indices
     5.6      start = end.foldLeft (start) ((s, t) => s + (t -> (s(t) + change.added.length - change.removed)))
     5.7 -    start = removed.foldLeft (start) ((s, t) => s - t)
     5.8  
     5.9      val split_begin = removed.takeWhile(start(_) < change.start).
    5.10 -      map (t => new Token(t.content.substring(0, change.start - start(t)),
    5.11 -                          t.kind))
    5.12 +      map (t => {
    5.13 +          val split_tok = new Token(t.content.substring(0, change.start - start(t)), t.kind)
    5.14 +          start += (split_tok -> start(t))
    5.15 +          split_tok
    5.16 +        })
    5.17 +
    5.18      val split_end = removed.dropWhile(stop(_) < change.start + change.removed).
    5.19 -      map (t => new Token(t.content.substring(change.start + change.removed - start(t)),
    5.20 -                          t.kind))
    5.21 +      map (t => {
    5.22 +          val split_tok = new Token(t.content.substring(change.start + change.removed - start(t)),
    5.23 +                          t.kind)
    5.24 +          start += (split_tok -> start(t))
    5.25 +          split_tok
    5.26 +        })
    5.27      // update indices
    5.28 -    start = split_end.foldLeft (start) ((s, t) => s + (t -> (change.start + change.added.length)))
    5.29 +    start = removed.foldLeft (start) ((s, t) => s - t)
    5.30 +    start = split_end.foldLeft (start) ((s, t) =>
    5.31 +    s + (t -> (change.start + change.added.length)))
    5.32  
    5.33      val ins = new Token(change.added, Token.Kind.OTHER)
    5.34      start += (ins -> change.start)
    5.35 @@ -121,77 +130,75 @@
    5.36      }
    5.37      val insert = new_tokens.reverse
    5.38      val new_token_list = begin ::: insert ::: old_suffix
    5.39 +    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
    5.40      token_changed(change.id,
    5.41                    begin.lastOption,
    5.42                    insert,
    5.43 -                  removed,
    5.44                    old_suffix.firstOption,
    5.45 -                  new_token_list,
    5.46 +                  new_tokenset,
    5.47                    start)
    5.48    }
    5.49    
    5.50    /** command view **/
    5.51  
    5.52    def find_command_at(pos: Int): Command = {
    5.53 -    for (cmd <- commands) { if (pos < cmd.stop) return cmd }
    5.54 +    for (cmd <- commands) { if (pos < cmd.stop(this)) return cmd }
    5.55      return null
    5.56    }
    5.57  
    5.58    private def token_changed(new_id: String,
    5.59                              before_change: Option[Token],
    5.60                              inserted_tokens: List[Token],
    5.61 -                            removed_tokens: List[Token],
    5.62                              after_change: Option[Token],
    5.63 -                            new_token_list: List[Token],
    5.64 +                            new_tokenset: LinearSet[Token],
    5.65                              new_token_start: Map[Token, Int]): (ProofDocument, StructureChange) =
    5.66    {
    5.67 -    val commands_list = List[Command]() ++ commands
    5.68 +    val cmd_first_changed =
    5.69 +      if (before_change.isDefined) commands.find(_.tokens.contains(before_change.get))
    5.70 +      else None
    5.71 +    val cmd_last_changed =
    5.72 +      if (after_change.isDefined) commands.find(_.tokens.contains(after_change.get))
    5.73 +      else None
    5.74  
    5.75 -    // calculate removed commands
    5.76 -    val first_removed = removed_tokens.firstOption
    5.77 +    val cmd_before_change =
    5.78 +      if (cmd_first_changed.isDefined) commands.prev(cmd_first_changed.get)
    5.79 +      else None
    5.80 +    val cmd_after_change =
    5.81 +      if (cmd_last_changed.isDefined) commands.next(cmd_last_changed.get)
    5.82 +      else None
    5.83  
    5.84 -    val (begin, remaining) =
    5.85 -      first_removed match {
    5.86 -        case None => (Nil, commands_list)
    5.87 -        case Some(fr) => commands_list.break(_.tokens.contains(fr))
    5.88 -      }
    5.89 -    val (removed_commands, end) =
    5.90 -      after_change match {
    5.91 -        case None => (remaining, Nil)
    5.92 -        case Some(ac) => remaining.break(_.tokens.contains(ac))
    5.93 -      }
    5.94 +    val removed_commands = commands.dropWhile(Some(_) != cmd_first_changed).
    5.95 +      takeWhile(Some(_) != cmd_after_change)
    5.96  
    5.97 +    // calculate inserted commands
    5.98      def tokens_to_commands(tokens: List[Token]): List[Command]= {
    5.99        tokens match {
   5.100          case Nil => Nil
   5.101          case t::ts =>
   5.102            val (cmd,rest) = ts.span(_.kind != Token.Kind.COMMAND_START)
   5.103 -          new Command(t::cmd) :: tokens_to_commands (rest)
   5.104 +          new Command(t::cmd, new_token_start) :: tokens_to_commands (rest)
   5.105        }
   5.106      }
   5.107  
   5.108 -    // calculate inserted commands
   5.109 -    val new_commands = tokens_to_commands(new_token_list)
   5.110 -    val new_tokenset = (LinearSet() ++ new_token_list).asInstanceOf[LinearSet[Token]]
   5.111 -    val new_commandset = (LinearSet() ++ (new_commands)).asInstanceOf[LinearSet[Command]]
   5.112 -    // drop known commands from the beginning
   5.113 -    val first_changed = before_change match {
   5.114 -      case None => new_tokenset.first_elem
   5.115 -      case Some(bc) => new_tokenset.next(bc)
   5.116 -    }
   5.117 -    val changed_commands = first_changed match {
   5.118 -      case None => Nil
   5.119 -      case Some(fc) => new_commands.dropWhile(!_.tokens.contains(fc))
   5.120 -    }
   5.121 -    val inserted_commands = after_change match {
   5.122 -      case None => changed_commands
   5.123 -      case Some(ac) => changed_commands.takeWhile(!_.tokens.contains(ac))
   5.124 -    }
   5.125 -    val change = new StructureChange(new_commands.find(_.tokens.contains(before_change)),
   5.126 -                                     inserted_commands, removed_commands)
   5.127 +    val split_begin_tokens =
   5.128 +      if (!cmd_first_changed.isDefined || !before_change.isDefined) Nil
   5.129 +      else {
   5.130 +        cmd_first_changed.get.tokens.takeWhile(_ != before_change.get) ::: List(before_change.get)
   5.131 +      }
   5.132 +    val split_end_tokens =
   5.133 +      if (!cmd_last_changed.isDefined || !after_change.isDefined) Nil
   5.134 +      else {
   5.135 +        cmd_last_changed.get.tokens.dropWhile(_ != after_change.get)
   5.136 +      }
   5.137 +
   5.138 +    val rescanning_tokens = split_begin_tokens ::: inserted_tokens ::: split_end_tokens
   5.139 +    val inserted_commands = tokens_to_commands(rescanning_tokens)
   5.140 +
   5.141 +    val change = new StructureChange(cmd_before_change, inserted_commands, removed_commands.toList)
   5.142      // build new document
   5.143 -    var new_commands = commands
   5.144 -    while(new_commands.next())
   5.145 +    val new_commandset = commands.delete_between(cmd_before_change, cmd_after_change).
   5.146 +        insert_after(cmd_before_change, inserted_commands)
   5.147 +
   5.148      val doc =
   5.149        new ProofDocument(new_id, new_tokenset, new_token_start, new_commandset, active, is_command_keyword)
   5.150      return (doc, change)

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

     7.1 --- a/src/Tools/jEdit/src/prover/Command.scala	Mon Apr 20 20:28:45 2009 +0200
     7.2 +++ b/src/Tools/jEdit/src/prover/Command.scala	Wed Apr 22 17:35:49 2009 +0200
     7.3 @@ -29,7 +29,7 @@
     7.4  }
     7.5  
     7.6  
     7.7 -class Command(val tokens: List[Token])
     7.8 +class Command(val tokens: List[Token], val starts: Map[Token, Int])
     7.9  {
    7.10    val id = Isabelle.plugin.id()
    7.11  
    7.12 @@ -38,10 +38,10 @@
    7.13    override def toString = name
    7.14  
    7.15    val name = tokens.head.content
    7.16 -  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT))
    7.17 +  val content:String = Token.string_from_tokens(tokens.takeWhile(_.kind != Token.Kind.COMMENT), starts)
    7.18  
    7.19 -  def start = tokens.first.start
    7.20 -  def stop = tokens.last.stop
    7.21 +  def start(doc: ProofDocument) = doc.token_start(tokens.first)
    7.22 +  def stop(doc: ProofDocument) = doc.token_start(tokens.last) + tokens.last.length
    7.23  
    7.24    /* command status */
    7.25  
    7.26 @@ -80,10 +80,14 @@
    7.27    /* markup */
    7.28  
    7.29    val root_node =
    7.30 -    new MarkupNode(this, 0, stop - start, id, Markup.COMMAND_SPAN, content)
    7.31 +    new MarkupNode(this, 0, starts(tokens.last) - starts(tokens.first) + tokens.last.length, id, Markup.COMMAND_SPAN, content)
    7.32  
    7.33 -  def node_from(kind: String, begin: Int, end: Int) = {
    7.34 -    val markup_content = content.substring(begin, end)
    7.35 -    new MarkupNode(this, begin, end, id, kind, markup_content)
    7.36 +  def add_markup(kind: String, begin: Int, end: Int) = {
    7.37 +    val markup_content = if (end <= content.length) content.substring(begin, end)
    7.38 +      else {
    7.39 +        System.err.println (root_node.stop, content, content.length, end)
    7.40 +        "wrong indices?"
    7.41 +      }
    7.42 +    root_node insert new MarkupNode(this, begin, end, id, kind, markup_content)
    7.43    }
    7.44  }

     8.1 --- a/src/Tools/jEdit/src/prover/MarkupNode.scala	Mon Apr 20 20:28:45 2009 +0200
     8.2 +++ b/src/Tools/jEdit/src/prover/MarkupNode.scala	Wed Apr 22 17:35:49 2009 +0200
     8.3 @@ -6,6 +6,8 @@
     8.4  
     8.5  package isabelle.prover
     8.6  
     8.7 +import isabelle.proofdocument.ProofDocument
     8.8 +
     8.9  import sidekick.IAsset
    8.10  import javax.swing._
    8.11  import javax.swing.text.Position
    8.12 @@ -13,10 +15,10 @@
    8.13  
    8.14  object MarkupNode {
    8.15  
    8.16 -  def markup2default_node(node : MarkupNode) : DefaultMutableTreeNode = {
    8.17 +  def markup2default_node(node: MarkupNode, cmd: Command, doc: ProofDocument) : DefaultMutableTreeNode = {
    8.18  
    8.19      implicit def int2pos(offset: Int): Position =
    8.20 -      new Position { def getOffset = offset }
    8.21 +      new Position { def getOffset = offset; override def toString = offset.toString}
    8.22  
    8.23      object RelativeAsset extends IAsset {
    8.24        override def getIcon : Icon = null
    8.25 @@ -25,10 +27,10 @@
    8.26        override def getName : String = node.id
    8.27        override def setName (name : String) = ()
    8.28        override def setStart(start : Position) = ()
    8.29 -      override def getStart : Position = node.abs_start
    8.30 +      override def getStart : Position = node.abs_start(doc)
    8.31        override def setEnd(end : Position) = ()
    8.32 -      override def getEnd : Position = node.abs_stop
    8.33 -      override def toString = node.id + ": " + node.kind + "[" + node.start + " - " + node.stop + "]"
    8.34 +      override def getEnd : Position = node.abs_stop(doc)
    8.35 +      override def toString = node.id + ": " + node.kind + "[" + getStart + " - " + getEnd + "]"
    8.36      }
    8.37  
    8.38      new DefaultMutableTreeNode(RelativeAsset)
    8.39 @@ -38,40 +40,27 @@
    8.40  class MarkupNode (val base : Command, val start : Int, val stop : Int,
    8.41                      val id : String, val kind : String, val desc : String) {
    8.42  
    8.43 -  val swing_node : DefaultMutableTreeNode = MarkupNode.markup2default_node (this)
    8.44 +  def swing_node(doc: ProofDocument) : DefaultMutableTreeNode = {
    8.45 +    val node = MarkupNode.markup2default_node (this, base, doc)
    8.46 +    for (c <- children) node add c.swing_node(doc)
    8.47 +    node
    8.48 +  }
    8.49 +    
    8.50 +  def abs_start(doc: ProofDocument) = base.start(doc) + start
    8.51 +  def abs_stop(doc: ProofDocument) = base.start(doc) + stop
    8.52  
    8.53    var parent : MarkupNode = null
    8.54    def orphan = parent == null
    8.55  
    8.56 -  def length = stop - start
    8.57 -  def abs_start = base.start + start
    8.58 -  def abs_stop = base.start + stop
    8.59 -
    8.60 -  private var children_cell : List[MarkupNode] = Nil
    8.61 -  //track changes in swing_node
    8.62 -  def children = children_cell
    8.63 -  def children_= (cs : List[MarkupNode]) = {
    8.64 -    swing_node.removeAllChildren
    8.65 -    for (c <- cs) swing_node add c.swing_node
    8.66 -    children_cell = cs
    8.67 -  }
    8.68 +  var children : List[MarkupNode] = Nil
    8.69  
    8.70    private def add(child : MarkupNode) {
    8.71      child parent = this
    8.72 -    children_cell = (child :: children) sort ((a, b) => a.start < b.start)
    8.73 -
    8.74 -    swing_node add child.swing_node
    8.75 +    children = (child :: children) sort ((a, b) => a.start < b.start)
    8.76    }
    8.77  
    8.78    private def remove(nodes : List[MarkupNode]) {
    8.79 -    children_cell = children diff nodes
    8.80 -
    8.81 -      for (node <- nodes) try {
    8.82 -        swing_node remove node.swing_node
    8.83 -      } catch { case e : IllegalArgumentException =>
    8.84 -        System.err.println(e.toString)
    8.85 -        case e => throw e
    8.86 -      }
    8.87 +    children = children diff nodes
    8.88    }
    8.89  
    8.90    def dfs : List[MarkupNode] = {

     9.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Apr 20 20:28:45 2009 +0200
     9.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Wed Apr 22 17:35:49 2009 +0200
     9.3 @@ -190,7 +190,7 @@
     9.4                        // inner syntax: id from props
     9.5                        else command
     9.6                      if (cmd != null) {
     9.7 -                      cmd.root_node.insert(cmd.node_from(kind, begin, end))
     9.8 +                      cmd.add_markup(kind, begin, end)
     9.9                        command_change(cmd)
    9.10                      }
    9.11                    case _ =>
    9.12 @@ -249,7 +249,7 @@
    9.13        for (cmd <- changes.removed_commands) yield {
    9.14          commands -= cmd.id
    9.15          if (cmd.state_id != null) states -= cmd.state_id
    9.16 -        (document.commands.prev(cmd).map(_.id).getOrElse(document_id0)) -> None
    9.17 +        changes.before_change.map(_.id).getOrElse(document_id0) -> None
    9.18        }
    9.19      val inserts =
    9.20        for (cmd <- changes.added_commands) yield {

    10.1 --- a/src/Tools/jEdit/src/utils/LinearSet.scala	Mon Apr 20 20:28:45 2009 +0200
    10.2 +++ b/src/Tools/jEdit/src/utils/LinearSet.scala	Wed Apr 22 17:35:49 2009 +0200
    10.3 @@ -43,7 +43,7 @@
    10.4    def contains(elem: A): Boolean =
    10.5      !isEmpty && (last_elem.get == elem || body.isDefinedAt(elem))
    10.6  
    10.7 -  def insert_after(hook: Option[A], elem: A): LinearSet[A] =
    10.8 +  private def _insert_after(hook: Option[A], elem: A): LinearSet[A] =
    10.9      if (contains(elem)) throw new LinearSet.Duplicate(elem.toString)
   10.10      else hook match {
   10.11        case Some(hook) =>
   10.12 @@ -55,8 +55,11 @@
   10.13          if (isEmpty) LinearSet.make(Some(elem), Some(elem), Map.empty)
   10.14          else LinearSet.make(Some(elem), last_elem, body + (elem -> first_elem.get))
   10.15      }
   10.16 -    
   10.17 -  def +(elem: A): LinearSet[A] = insert_after(last_elem, elem)
   10.18 +
   10.19 +  def insert_after(hook: Option[A], elems: Seq[A]): LinearSet[A] =
   10.20 +    elems.reverse.foldLeft (this) ((ls, elem) => ls._insert_after(hook, elem))
   10.21 +
   10.22 +  def +(elem: A): LinearSet[A] = _insert_after(last_elem, elem)
   10.23  
   10.24    def delete_after(elem: Option[A]): LinearSet[A] =
   10.25      elem match {
   10.26 @@ -70,7 +73,18 @@
   10.27          else if (size == 1) empty
   10.28          else LinearSet.make(Some(body(first_elem.get)), last_elem, body - first_elem.get)
   10.29      }
   10.30 -    
   10.31 +
   10.32 +  def delete_between(from: Option[A], to: Option[A]): LinearSet[A] = {
   10.33 +    if(!first_elem.isDefined) this
   10.34 +    else {
   10.35 +      val next = if (from == last_elem) None
   10.36 +                 else if (from == None) first_elem
   10.37 +                 else from.map(body(_))
   10.38 +      if (next == to) this
   10.39 +      else delete_after(from).delete_between(from, to)
   10.40 +    }
   10.41 +  }
   10.42 +
   10.43    def -(elem: A): LinearSet[A] =
   10.44      if (!contains(elem)) throw new LinearSet.Undefined(elem.toString)
   10.45      else delete_after(body find (p => p._2 == elem) map (p => p._1))