# HG changeset patch
# User immler@in.tum.de
# Date 1228935155 -3600
# Node ID 6c812a3cb170e99855790cb61df7ac012959793d
# Parent  bd8d70cd9baff77b4fd4d6c620aad70012a4e7a5
information on command-phase left of scrollbar (with panel)

diff -r bd8d70cd9baf -r 6c812a3cb170 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala	Wed Dec 10 19:52:35 2008 +0100
@@ -0,0 +1,116 @@
+/*
+ * ErrorOverview.java - Error overview component
+ * :tabSize=8:indentSize=8:noTabs=false:
+ * :folding=explicit:collapseFolds=1:
+ *
+ * Copyright (C) 2003 Slava Pestov
+ *
+ * This program is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.
+ */
+
+package isabelle.jedit
+
+import isabelle.prover.Command
+
+import javax.swing._
+import java.awt.event._
+import java.awt._
+import org.gjt.sp.jedit.gui.RolloverButton;
+import org.gjt.sp.jedit.textarea.JEditTextArea;
+import org.gjt.sp.jedit._
+
+class PhaseOverviewPanel(textarea : JEditTextArea) extends JPanel(new BorderLayout) {
+
+  private val WIDTH = 10
+	private val HILITE_HEIGHT = 2
+
+  Plugin.plugin.prover.commandInfo.add(_ => repaint())
+  setRequestFocusEnabled(false);
+
+  addMouseListener(new MouseAdapter {
+    override def mousePressed(evt : MouseEvent) {
+      val line = yToLine(evt.getY)
+      if(line >= 0 && line < textarea.getLineCount())
+        textarea.setCaretPosition(textarea.getLineStartOffset(line))
+    }
+  })
+
+	override def addNotify	{
+		super.addNotify();
+		ToolTipManager.sharedInstance.registerComponent(this);
+	}
+
+	override def removeNotify()
+	{
+		super.removeNotify
+		ToolTipManager.sharedInstance.unregisterComponent(this);
+	}
+
+	override def getToolTipText(evt : MouseEvent) : String =
+	{
+		val buffer = textarea.getBuffer
+		val lineCount = buffer.getLineCount
+		val line = yToLine(evt.getY())
+		if(line >= 0 && line < textarea.getLineCount)
+		{
+      "TODO: Tooltip"
+    } else ""
+	}
+
+	override def paintComponent(gfx : Graphics) {
+		super.paintComponent(gfx)
+
+
+		val buffer = textarea.getBuffer
+
+		val line_count = buffer.getLineCount
+
+    for(command <- Plugin.plugin.prover.document.commands) {
+      val line1 = buffer.getLineOfOffset(command.start)
+      val line2 = buffer.getLineOfOffset(command.stop - 1) + 1
+      if(line1 < 0 || line2 > line_count){
+        System.err.println("invalid line numbers: " + line1 + " - " + line2)
+      } else {
+        val y1 = lineToY(line1)
+        val y2 = lineToY(line2) - 1
+        val linelength = buffer.getLineLength(line1)
+        val color = command.phase match {
+          case Command.Phase.UNPROCESSED => Color.yellow
+          case Command.Phase.FINISHED => Color.green
+          case Command.Phase.FAILED => Color.red
+        }
+				gfx.setColor(color)
+				gfx.fillRect(0, y1, getWidth, 1 max y2 - y1)
+			}
+		}
+	}
+
+	override def getPreferredSize : Dimension =
+	{
+		new Dimension(10,0)
+	}
+
+
+	private def lineToY(line : Int) : Int =
+	{
+		(line * getHeight) / textarea.getBuffer.getLineCount
+	}
+
+	private def yToLine(y : Int) : Int =
+	{
+		(y * textarea.getBuffer.getLineCount) / getHeight
+	}
+
+}
\ No newline at end of file