src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
author immler@in.tum.de
Mon Dec 15 16:23:17 2008 +0100 (2008-12-15)
changeset 34404 98155c35d252
parent 34403 6c812a3cb170
child 34405 a67a4eaebcff
permissions -rw-r--r--
delayed repainting new phase in buffer and overview;
reverted johannes' handling of removed Commands
immler@34403
     1
/*
immler@34403
     2
 * ErrorOverview.java - Error overview component
immler@34403
     3
 * :tabSize=8:indentSize=8:noTabs=false:
immler@34403
     4
 * :folding=explicit:collapseFolds=1:
immler@34403
     5
 *
immler@34403
     6
 * Copyright (C) 2003 Slava Pestov
immler@34403
     7
 *
immler@34403
     8
 * This program is free software; you can redistribute it and/or
immler@34403
     9
 * modify it under the terms of the GNU General Public License
immler@34403
    10
 * as published by the Free Software Foundation; either version 2
immler@34403
    11
 * of the License, or any later version.
immler@34403
    12
 *
immler@34403
    13
 * This program is distributed in the hope that it will be useful,
immler@34403
    14
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
immler@34403
    15
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
immler@34403
    16
 * GNU General Public License for more details.
immler@34403
    17
 *
immler@34403
    18
 * You should have received a copy of the GNU General Public License
immler@34403
    19
 * along with this program; if not, write to the Free Software
immler@34403
    20
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
immler@34403
    21
 */
immler@34403
    22
immler@34403
    23
package isabelle.jedit
immler@34403
    24
immler@34403
    25
import isabelle.prover.Command
immler@34404
    26
import isabelle.utils.Delay
immler@34403
    27
immler@34403
    28
import javax.swing._
immler@34403
    29
import java.awt.event._
immler@34403
    30
import java.awt._
immler@34403
    31
import org.gjt.sp.jedit.gui.RolloverButton;
immler@34403
    32
import org.gjt.sp.jedit.textarea.JEditTextArea;
immler@34404
    33
import org.gjt.sp.jedit.buffer.JEditBuffer;
immler@34403
    34
import org.gjt.sp.jedit._
immler@34403
    35
immler@34403
    36
class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
immler@34403
    37
immler@34403
    38
  private val WIDTH = 10
immler@34403
    39
	private val HILITE_HEIGHT = 2
immler@34403
    40
immler@34404
    41
  Plugin.plugin.prover.commandInfo.add(cc => {
immler@34404
    42
      System.err.println(cc.command.idString + ": " + cc.command.phase)
immler@34404
    43
      paintCommand(cc.command,textarea.getBuffer, getGraphics)
immler@34404
    44
      System.err.println(cc.command.idString + ": " + cc.command.phase)
immler@34404
    45
    })
immler@34403
    46
  setRequestFocusEnabled(false);
immler@34403
    47
immler@34403
    48
  addMouseListener(new MouseAdapter {
immler@34403
    49
    override def mousePressed(evt : MouseEvent) {
immler@34403
    50
      val line = yToLine(evt.getY)
immler@34403
    51
      if(line >= 0 && line < textarea.getLineCount())
immler@34403
    52
        textarea.setCaretPosition(textarea.getLineStartOffset(line))
immler@34403
    53
    }
immler@34403
    54
  })
immler@34403
    55
immler@34403
    56
	override def addNotify	{
immler@34403
    57
		super.addNotify();
immler@34403
    58
		ToolTipManager.sharedInstance.registerComponent(this);
immler@34403
    59
	}
immler@34403
    60
immler@34403
    61
	override def removeNotify()
immler@34403
    62
	{
immler@34403
    63
		super.removeNotify
immler@34403
    64
		ToolTipManager.sharedInstance.unregisterComponent(this);
immler@34403
    65
	}
immler@34403
    66
immler@34403
    67
	override def getToolTipText(evt : MouseEvent) : String =
immler@34403
    68
	{
immler@34403
    69
		val buffer = textarea.getBuffer
immler@34403
    70
		val lineCount = buffer.getLineCount
immler@34403
    71
		val line = yToLine(evt.getY())
immler@34403
    72
		if(line >= 0 && line < textarea.getLineCount)
immler@34403
    73
		{
immler@34403
    74
      "TODO: Tooltip"
immler@34403
    75
    } else ""
immler@34403
    76
	}
immler@34403
    77
immler@34404
    78
  private def paintCommand(command : Command, buffer : JEditBuffer, gfx : Graphics) {
immler@34404
    79
      val line1 = buffer.getLineOfOffset(command.start)
immler@34404
    80
      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
immler@34404
    81
      val y = lineToY(line1)
immler@34404
    82
      val height = lineToY(line2) - y - 1
immler@34404
    83
      val (light, dark) = command.phase match {
immler@34404
    84
        case Command.Phase.UNPROCESSED => (Color.yellow, new Color(128,128,0))
immler@34404
    85
        case Command.Phase.FINISHED => (Color.green, new Color(0, 128, 0))
immler@34404
    86
        case Command.Phase.FAILED => (Color.red, new Color(128,0,0))
immler@34404
    87
      }
immler@34404
    88
immler@34404
    89
      gfx.setColor(light)
immler@34404
    90
      gfx.fillRect(0, y, getWidth - 1, 1 max height)
immler@34404
    91
      if(height > 2){
immler@34404
    92
        gfx.setColor(dark)
immler@34404
    93
        gfx.drawRect(0, y, getWidth - 1, height)
immler@34404
    94
      }
immler@34404
    95
immler@34404
    96
  }
immler@34404
    97
immler@34403
    98
	override def paintComponent(gfx : Graphics) {
immler@34403
    99
		super.paintComponent(gfx)
immler@34403
   100
immler@34403
   101
		val buffer = textarea.getBuffer
immler@34403
   102
immler@34404
   103
    for(c <- Plugin.plugin.prover.document.commands)
immler@34404
   104
      paintCommand(c, buffer, gfx)
immler@34403
   105
	}
immler@34403
   106
immler@34403
   107
	override def getPreferredSize : Dimension =
immler@34403
   108
	{
immler@34403
   109
		new Dimension(10,0)
immler@34403
   110
	}
immler@34403
   111
immler@34403
   112
immler@34403
   113
	private def lineToY(line : Int) : Int =
immler@34403
   114
	{
immler@34403
   115
		(line * getHeight) / textarea.getBuffer.getLineCount
immler@34403
   116
	}
immler@34403
   117
immler@34403
   118
	private def yToLine(y : Int) : Int =
immler@34403
   119
	{
immler@34403
   120
		(y * textarea.getBuffer.getLineCount) / getHeight
immler@34403
   121
	}
immler@34403
   122
immler@34403
   123
}