# HG changeset patch # User immler@in.tum.de # Date 1251363069 -7200 # Node ID acaac03ced000a443c8adfec49e0d7249ecfa464 # Parent 85222d00f5ec882519a8f1f039707b9e7a8083a9 tuned whitespace diff -r 85222d00f5ec -r acaac03ced00 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Aug 27 10:51:09 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Thu Aug 27 10:51:09 2009 +0200 @@ -25,7 +25,7 @@ { private val WIDTH = 10 - private val HILITE_HEIGHT = 2 + private val HILITE_HEIGHT = 2 val repaint_delay = Swing_Thread.delay(100){ repaint() } @@ -39,27 +39,27 @@ } }) - override def addNotify { - super.addNotify(); - ToolTipManager.sharedInstance.registerComponent(this); - } + override def addNotify { + super.addNotify(); + ToolTipManager.sharedInstance.registerComponent(this); + } - override def removeNotify() - { - super.removeNotify - ToolTipManager.sharedInstance.unregisterComponent(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) - { + 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 "" - } + } private def paintCommand(command : Command, buffer : JEditBuffer, doc: ProofDocument, gfx : Graphics) { val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc))) @@ -80,22 +80,22 @@ } } - override def paintComponent(gfx : Graphics) { - super.paintComponent(gfx) - val buffer = textarea.getBuffer +override def paintComponent(gfx : Graphics) { + super.paintComponent(gfx) + val buffer = textarea.getBuffer val theory_view = Isabelle.prover_setup(buffer).get.theory_view val document = theory_view.current_document() + for (c <- document.commands) paintCommand(c, buffer, document, gfx) + } - } - - override def getPreferredSize = new Dimension(10,0) +override def getPreferredSize = new Dimension(10,0) - private def lineToY(line : Int) : Int = - (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines) +private def lineToY(line : Int) : Int = + (line * getHeight) / (textarea.getBuffer.getLineCount max textarea.getVisibleLines) - private def yToLine(y : Int) : Int = - (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight +private def yToLine(y : Int) : Int = + (y * (textarea.getBuffer.getLineCount max textarea.getVisibleLines)) / getHeight } \ No newline at end of file