# HG changeset patch # User immler@in.tum.de # Date 1239040893 -7200 # Node ID b928628742edafc578fe845a282f386c7ba6df68 # Parent 56217d219e27fdfe90f3336f79f94be92825f453 implemented to_current and from_current in dependancy of document-versions diff -r 56217d219e27 -r b928628742ed src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala --- a/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Apr 06 19:04:38 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/DynamicTokenMarker.scala Mon Apr 06 20:01:33 2009 +0200 @@ -82,12 +82,12 @@ val current_document = prover.document - def to = Isabelle.prover_setup(buffer).get.theory_view.to_current(_) - def from = Isabelle.prover_setup(buffer).get.theory_view.from_current(_) + 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, _) var next_x = start for { - command <- prover.document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop)) + command <- current_document.commands.dropWhile(_.stop <= from(start)).takeWhile(_.start < from(stop)) markup <- command.root_node.flatten if(to(markup.abs_stop) > start) if(to(markup.abs_start) < stop) diff -r 56217d219e27 -r b928628742ed src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Apr 06 19:04:38 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Mon Apr 06 20:01:33 2009 +0200 @@ -17,7 +17,7 @@ import org.gjt.sp.jedit.buffer.JEditBuffer; import org.gjt.sp.jedit._ -class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) { +class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: (String, Int) => Int) extends JPanel(new BorderLayout) { private val WIDTH = 10 private val HILITE_HEIGHT = 2 @@ -57,9 +57,9 @@ } else "" } - private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) { - val line1 = buffer.getLineOfOffset(to_current(command.start)) - val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1 + 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 val y = lineToY(line1) val height = lineToY(line2) - y - 1 val (light, dark) = command.status match { @@ -81,8 +81,9 @@ super.paintComponent(gfx) val buffer = textarea.getBuffer - for (c <- prover.document.commands) - paintCommand(c, buffer, gfx) + val document = prover.document + for (c <- document.commands) + paintCommand(c, buffer, document.id, gfx) } diff -r 56217d219e27 -r b928628742ed src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Apr 06 19:04:38 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Mon Apr 06 20:01:33 2009 +0200 @@ -59,7 +59,7 @@ col_timer.setRepeats(true) - private val phase_overview = new PhaseOverviewPanel(prover, to_current(_)) + private val phase_overview = new PhaseOverviewPanel(prover, to_current) /* activation */ @@ -118,23 +118,40 @@ } }.start - def from_current (pos: Int) = - if (col != null && col.start <= pos) - if (pos < col.start + col.added.length) col.start - else pos - col.added.length + col.removed - else pos + def _from_current(to_id: String, changes: List[Text.Change], pos: Int): Int = + changes match { + case Nil => pos + case Text.Change(id, start, added, removed) :: rest_changes => { + val shifted = if (start <= pos) + if (pos < start + added.length) start + else pos - added.length + removed + else pos + if (id == to_id) shifted + else _from_current(to_id, rest_changes, shifted) + } + } - def to_current (pos : Int) = - if (col != null && col.start <= pos) - if (pos < col.start + col.removed) col.start - else pos + col.added.length - col.removed - else pos + def _to_current(from_id: String, changes: List[Text.Change], pos: Int): Int = + changes match { + case Nil => pos + case Text.Change(id, start, added, removed) :: rest_changes => { + val shifted = if (id == from_id) pos else _to_current(from_id, rest_changes, pos) + if (start <= shifted) + if (shifted < start + removed) start + else shifted + added.length - removed + else shifted + } + } + + def to_current(from_id: String, pos : Int) = _to_current(from_id, changes, pos) + def from_current(to_id: String, pos : Int) = _from_current(to_id, changes, pos) def repaint(cmd: Command) = { + val document = prover.document if (text_area != null) { - val start = text_area.getLineOfOffset(to_current(cmd.start)) - val stop = text_area.getLineOfOffset(to_current(cmd.stop) - 1) + val start = text_area.getLineOfOffset(to_current(document.id, cmd.start)) + val stop = text_area.getLineOfOffset(to_current(document.id, cmd.stop) - 1) text_area.invalidateLineRange(start, stop) if (Isabelle.prover_setup(buffer).get.selected_state == cmd) @@ -174,11 +191,14 @@ override def paintValidLine(gfx: Graphics2D, screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int) = { + val document = prover.document + def from_current(pos: Int) = this.from_current(document.id, pos) + def to_current(pos: Int) = this.to_current(document.id, pos) val saved_color = gfx.getColor val metrics = text_area.getPainter.getFontMetrics - var e = prover.document.find_command_at(from_current(start)) - val commands = prover.document.commands.dropWhile(_.stop <= from_current(start)). + 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) // encolor phase for (e <- commands) { @@ -202,9 +222,13 @@ /* BufferListener methods */ + private var changes: List[Text.Change] = Nil + private def commit { - if (col != null) + if (col != null) { + changes += col document_actor ! col + } col = null if (col_timer.isRunning()) col_timer.stop()