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