1.1 --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 06 19:04:38 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala	Mon Apr 06 20:01:33 2009 +0200
     1.3 @@ -82,12 +82,12 @@
     1.4  
     1.5      val current_document = prover.document
     1.6     
     1.7 -    def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_)
     1.8 -    def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_)
     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  
    1.12      var next_x = start
    1.13      for {
    1.14 -      command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
    1.15 +      command <- current_document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop))
    1.16        markup <- command.root_node.flatten
    1.17        if(to(markup.abs_stop) > start)
    1.18        if(to(markup.abs_start) < stop)

     2.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Apr 06 19:04:38 2009 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Apr 06 20:01:33 2009 +0200
     2.3 @@ -17,7 +17,7 @@
     2.4  import org.gjt.sp.jedit.buffer.JEditBuffer;
     2.5  import org.gjt.sp.jedit._
     2.6  
     2.7 -class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) {
     2.8 +class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: (String, Int) => Int) extends JPanel(new BorderLayout) {
     2.9  
    2.10    private val WIDTH = 10
    2.11  	private val HILITE_HEIGHT = 2
    2.12 @@ -57,9 +57,9 @@
    2.13      } else ""
    2.14  	}
    2.15  
    2.16 -  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
    2.17 -      val line1 = buffer.getLineOfOffset(to_current(command.start))
    2.18 -      val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1
    2.19 +  private def paintCommand(command : Command, buffer : JEditBuffer, doc_id: String, gfx : Graphics) {
    2.20 +      val line1 = buffer.getLineOfOffset(to_current(doc_id, command.start))
    2.21 +      val line2 = buffer.getLineOfOffset(to_current(doc_id, command.stop - 1)) + 1
    2.22        val y = lineToY(line1)
    2.23        val height = lineToY(line2) - y - 1
    2.24        val (light, dark) = command.status match {
    2.25 @@ -81,8 +81,9 @@
    2.26  		super.paintComponent(gfx)
    2.27  
    2.28  		val buffer = textarea.getBuffer
    2.29 -    for (c <- prover.document.commands)
    2.30 -      paintCommand(c, buffer, gfx)
    2.31 +    val document = prover.document
    2.32 +    for (c <- document.commands)
    2.33 +      paintCommand(c, buffer, document.id, gfx)
    2.34  
    2.35  	}
    2.36  

     3.1 --- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 06 19:04:38 2009 +0200
     3.2 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Mon Apr 06 20:01:33 2009 +0200
     3.3 @@ -59,7 +59,7 @@
     3.4    col_timer.setRepeats(true)
     3.5  
     3.6  
     3.7 -  private val phase_overview = new PhaseOverviewPanel(prover, to_current(_))
     3.8 +  private val phase_overview = new PhaseOverviewPanel(prover, to_current)
     3.9  
    3.10  
    3.11    /* activation */
    3.12 @@ -118,23 +118,40 @@
    3.13      }
    3.14    }.start
    3.15  
    3.16 -  def from_current (pos: Int) =
    3.17 -    if (col != null && col.start <= pos)
    3.18 -      if (pos < col.start + col.added.length) col.start
    3.19 -      else pos - col.added.length + col.removed
    3.20 -    else pos
    3.21 +  def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int =
    3.22 +    changes match {
    3.23 +      case Nil => pos
    3.24 +      case Text.Change(id, start, added, removed) :: rest_changes => {
    3.25 +        val shifted = if (start <= pos)
    3.26 +            if (pos < start + added.length) start
    3.27 +            else pos - added.length + removed
    3.28 +          else pos
    3.29 +        if (id == to_id) shifted
    3.30 +        else _from_current(to_id, rest_changes, shifted)
    3.31 +      }
    3.32 +    }
    3.33  
    3.34 -  def to_current (pos : Int) =
    3.35 -    if (col != null && col.start <= pos)
    3.36 -      if (pos < col.start + col.removed) col.start
    3.37 -      else pos + col.added.length - col.removed
    3.38 -    else pos
    3.39 +  def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int =
    3.40 +    changes match {
    3.41 +      case Nil => pos
    3.42 +      case Text.Change(id, start, added, removed) :: rest_changes => {
    3.43 +        val shifted = if (id == from_id) pos else _to_current(from_id, rest_changes, pos)
    3.44 +        if (start <= shifted)
    3.45 +          if (shifted < start + removed) start
    3.46 +          else shifted + added.length - removed
    3.47 +        else shifted
    3.48 +      }
    3.49 +    }
    3.50 +
    3.51 +  def to_current(from_id: String, pos : Int) = _to_current(from_id, changes, pos)
    3.52 +  def from_current(to_id: String, pos : Int) = _from_current(to_id, changes, pos)
    3.53  
    3.54    def repaint(cmd: Command) =
    3.55    {
    3.56 +    val document = prover.document
    3.57      if (text_area != null) {
    3.58 -      val start = text_area.getLineOfOffset(to_current(cmd.start))
    3.59 -      val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1)
    3.60 +      val start = text_area.getLineOfOffset(to_current(document.id, cmd.start))
    3.61 +      val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1)
    3.62        text_area.invalidateLineRange(start, stop)
    3.63  
    3.64        if (Isabelle.prover_setup(buffer).get.selected_state == cmd)
    3.65 @@ -174,11 +191,14 @@
    3.66    override def paintValidLine(gfx: Graphics2D,
    3.67      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) =
    3.68    {
    3.69 +    val document = prover.document
    3.70 +    def from_current(pos: Int) = this.from_current(document.id, pos)
    3.71 +    def to_current(pos: Int) = this.to_current(document.id, pos)
    3.72      val saved_color = gfx.getColor
    3.73  
    3.74      val metrics = text_area.getPainter.getFontMetrics
    3.75 -    var e = prover.document.find_command_at(from_current(start))
    3.76 -    val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)).
    3.77 +    var e = document.find_command_at(from_current(start))
    3.78 +    val commands = document.commands.dropWhile(_.stop <= from_current(start)).
    3.79        takeWhile(c => to_current(c.start) < end)
    3.80      // encolor phase
    3.81      for (e <- commands) {
    3.82 @@ -202,9 +222,13 @@
    3.83  
    3.84    /* BufferListener methods */
    3.85  
    3.86 +  private var changes: List[Text.Change] = Nil
    3.87 +
    3.88    private def commit {
    3.89 -    if (col != null)
    3.90 +    if (col != null) {
    3.91 +      changes += col
    3.92        document_actor ! col
    3.93 +    }
    3.94      col = null
    3.95      if (col_timer.isRunning())
    3.96        col_timer.stop()