# HG changeset patch
# User immler@in.tum.de
# Date 1233490476 -3600
# Node ID 411017e76e982ae8d13fdf16c05b9ed1ed0a6179
# Parent  14d70378f1c7a7abda6c31c3dd55f1cc749c16af
respect current offsets

diff -r 14d70378f1c7 -r 411017e76e98 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sun Feb 01 12:50:21 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Sun Feb 01 13:14:36 2009 +0100
@@ -17,7 +17,7 @@
 import org.gjt.sp.jedit.buffer.JEditBuffer;
 import org.gjt.sp.jedit._
 
-class PhaseOverviewPanel(prover : isabelle.prover.Prover) extends JPanel(new BorderLayout) {
+class PhaseOverviewPanel(prover: isabelle.prover.Prover, to_current: Int => Int) extends JPanel(new BorderLayout) {
 
   private val WIDTH = 10
 	private val HILITE_HEIGHT = 2
@@ -25,7 +25,7 @@
 
   val repaint_delay = new isabelle.utils.Delay(100, () => repaint())
   prover.command_info += (_ => repaint_delay.delay_or_ignore())
-    
+
   setRequestFocusEnabled(false);
 
   addMouseListener(new MouseAdapter {
@@ -59,8 +59,8 @@
 	}
 
   private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
-      val line1 = buffer.getLineOfOffset(command.start)
-      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
+      val line1 = buffer.getLineOfOffset(to_current(command.start))
+      val line2 = buffer.getLineOfOffset(to_current(command.stop - 1)) + 1
       val y = lineToY(line1)
       val height = lineToY(line2) - y - 1
       val (light, dark) = command.status match {
@@ -84,7 +84,7 @@
 		val buffer = textarea.getBuffer
     for (c <- prover.document.commands)
       paintCommand(c, buffer, gfx)
-    
+
 	}
 
 	override def getPreferredSize : Dimension =
diff -r 14d70378f1c7 -r 411017e76e98 src/Tools/jEdit/src/jedit/TheoryView.scala
--- a/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Feb 01 12:50:21 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/TheoryView.scala	Sun Feb 01 13:14:36 2009 +0100
@@ -85,7 +85,7 @@
   col_timer.setRepeats(true)
 
 
-  private val phase_overview = new PhaseOverviewPanel(prover)
+  private val phase_overview = new PhaseOverviewPanel(prover, to_current(_))
 
 
   /* activation */