src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
changeset 34404 98155c35d252
parent 34403 6c812a3cb170
child 34405 a67a4eaebcff
     1.1 --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Dec 10 19:52:35 2008 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Mon Dec 15 16:23:17 2008 +0100
     1.3 @@ -23,12 +23,14 @@
     1.4  package isabelle.jedit
     1.5  
     1.6  import isabelle.prover.Command
     1.7 +import isabelle.utils.Delay
     1.8  
     1.9  import javax.swing._
    1.10  import java.awt.event._
    1.11  import java.awt._
    1.12  import org.gjt.sp.jedit.gui.RolloverButton;
    1.13  import org.gjt.sp.jedit.textarea.JEditTextArea;
    1.14 +import org.gjt.sp.jedit.buffer.JEditBuffer;
    1.15  import org.gjt.sp.jedit._
    1.16  
    1.17  class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
    1.18 @@ -36,7 +38,11 @@
    1.19    private val WIDTH = 10
    1.20  	private val HILITE_HEIGHT = 2
    1.21  
    1.22 -  Plugin.plugin.prover.commandInfo.add(_ => repaint())
    1.23 +  Plugin.plugin.prover.commandInfo.add(cc => {
    1.24 +      System.err.println(cc.command.idString + ": " + cc.command.phase)
    1.25 +      paintCommand(cc.command,textarea.getBuffer, getGraphics)
    1.26 +      System.err.println(cc.command.idString + ": " + cc.command.phase)
    1.27 +    })
    1.28    setRequestFocusEnabled(false);
    1.29  
    1.30    addMouseListener(new MouseAdapter {
    1.31 @@ -69,32 +75,33 @@
    1.32      } else ""
    1.33  	}
    1.34  
    1.35 +  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
    1.36 +      val line1 = buffer.getLineOfOffset(command.start)
    1.37 +      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
    1.38 +      val y = lineToY(line1)
    1.39 +      val height = lineToY(line2) - y - 1
    1.40 +      val (light, dark) = command.phase match {
    1.41 +        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
    1.42 +        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
    1.43 +        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
    1.44 +      }
    1.45 +
    1.46 +      gfx.setColor(light)
    1.47 +      gfx.fillRect(0, y, getWidth - 1, 1 max height)
    1.48 +      if(height > 2){
    1.49 +        gfx.setColor(dark)
    1.50 +        gfx.drawRect(0, y, getWidth - 1, height)
    1.51 +      }
    1.52 +
    1.53 +  }
    1.54 +
    1.55  	override def paintComponent(gfx : Graphics) {
    1.56  		super.paintComponent(gfx)
    1.57  
    1.58 -
    1.59  		val buffer = textarea.getBuffer
    1.60  
    1.61 -		val line_count = buffer.getLineCount
    1.62 -
    1.63 -    for(command <- Plugin.plugin.prover.document.commands) {
    1.64 -      val line1 = buffer.getLineOfOffset(command.start)
    1.65 -      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
    1.66 -      if(line1 < 0 || line2 > line_count){
    1.67 -        System.err.println("invalid line numbers: " + line1 + " - " + line2)
    1.68 -      } else {
    1.69 -        val y1 = lineToY(line1)
    1.70 -        val y2 = lineToY(line2) - 1
    1.71 -        val linelength = buffer.getLineLength(line1)
    1.72 -        val color = command.phase match {
    1.73 -          case Command.Phase.UNPROCESSED => Color.yellow
    1.74 -          case Command.Phase.FINISHED => Color.green
    1.75 -          case Command.Phase.FAILED => Color.red
    1.76 -        }
    1.77 -				gfx.setColor(color)
    1.78 -				gfx.fillRect(0, y1, getWidth, 1 max y2 - y1)
    1.79 -			}
    1.80 -		}
    1.81 +    for(c <- Plugin.plugin.prover.document.commands)
    1.82 +      paintCommand(c, buffer, gfx)
    1.83  	}
    1.84  
    1.85  	override def getPreferredSize : Dimension =