--- 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)
--- 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)
}
--- 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()