# HG changeset patch # User wenzelm # Date 1253040320 -7200 # Node ID ff7734c8bdb7ee1ae501982956cb2c1177958ba3 # Parent 2997f2a0f8314871931a0148673f08b55a8e4950 renamed PhaseOverviewPanel to Document_Overview; diff -r 2997f2a0f831 -r ff7734c8bdb7 src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala --- a/src/Tools/jEdit/src/jedit/PhaseOverviewPanel.scala Tue Sep 15 20:39:00 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,82 +0,0 @@ -/* - * Information on command status left of scrollbar (with panel) - * - * @author Fabian Immler, TU Munich - */ - -package isabelle.jedit - -import isabelle.prover.{Prover, Command} -import isabelle.proofdocument.ProofDocument - -import javax.swing.{JPanel, ToolTipManager} -import java.awt.event.{MouseAdapter, MouseEvent} -import java.awt.{BorderLayout, Graphics, Dimension} - -import org.gjt.sp.jedit.gui.RolloverButton -import org.gjt.sp.jedit.textarea.JEditTextArea -import org.gjt.sp.jedit.buffer.JEditBuffer - - -class PhaseOverviewPanel( - prover: Prover, - text_area: JEditTextArea, - to_current: (ProofDocument, Int) => Int) - extends JPanel(new BorderLayout) -{ - private val WIDTH = 10 - private val HEIGHT = 2 - - setRequestFocusEnabled(false) - - addMouseListener(new MouseAdapter { - override def mousePressed(event: MouseEvent) { - val line = y_to_line(event.getY) - if (line >= 0 && line < text_area.getLineCount) - text_area.setCaretPosition(text_area.getLineStartOffset(line)) - } - }) - - override def addNotify() { - super.addNotify() - ToolTipManager.sharedInstance.registerComponent(this) - } - - override def removeNotify() { - super.removeNotify - ToolTipManager.sharedInstance.unregisterComponent(this) - } - - override def getToolTipText(event: MouseEvent): String = - { - val buffer = text_area.getBuffer - val lineCount = buffer.getLineCount - val line = y_to_line(event.getY()) - if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip" - else "" - } - - override def paintComponent(gfx: Graphics) { - super.paintComponent(gfx) - val buffer = text_area.getBuffer - val theory_view = Isabelle.prover_setup(buffer).get.theory_view - val doc = theory_view.current_document() - - for (command <- doc.commands) { - val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc))) - val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1 - val y = line_to_y(line1) - val height = HEIGHT * (line2 - line1) - gfx.setColor(TheoryView.choose_color(command, doc)) - gfx.fillRect(0, y, getWidth - 1, height) - } - } - - override def getPreferredSize = new Dimension(WIDTH, 0) - - private def line_to_y(line: Int): Int = - (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) - - private def y_to_line(y: Int): Int = - (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight -} \ No newline at end of file diff -r 2997f2a0f831 -r ff7734c8bdb7 src/Tools/jEdit/src/jedit/TheoryView.scala --- a/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Sep 15 20:39:00 2009 +0200 +++ b/src/Tools/jEdit/src/jedit/TheoryView.scala Tue Sep 15 20:45:20 2009 +0200 @@ -53,7 +53,7 @@ if (text_area.getBuffer == buffer) { update_syntax(command) invalidate_line(command) - phase_overview.repaint() + overview.repaint() } }) @@ -151,7 +151,7 @@ /* activation */ - private val phase_overview = new PhaseOverviewPanel(prover, text_area, to_current) + private val overview = new Document_Overview(prover, text_area, to_current) private val selected_state_controller = new CaretListener { override def caretUpdate(e: CaretEvent) { @@ -168,7 +168,7 @@ def activate() { text_area.addCaretListener(selected_state_controller) - text_area.addLeftOfScrollBar(phase_overview) + text_area.addLeftOfScrollBar(overview) text_area.getPainter. addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension) buffer.setTokenMarker(new DynamicTokenMarker(buffer, prover)) @@ -189,7 +189,7 @@ buffer.setTokenMarker(buffer.getMode.getTokenMarker) buffer.removeBufferListener(buffer_listener) text_area.getPainter.removeExtension(text_area_extension) - text_area.removeLeftOfScrollBar(phase_overview) + text_area.removeLeftOfScrollBar(overview) text_area.removeCaretListener(selected_state_controller) } @@ -245,7 +245,7 @@ // invoke repaint buffer.propertiesChanged() invalidate_all() - phase_overview.repaint() + overview.repaint() // track changes in buffer buffer.addBufferListener(buffer_listener) diff -r 2997f2a0f831 -r ff7734c8bdb7 src/Tools/jEdit/src/jedit/document_overview.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src/jedit/document_overview.scala Tue Sep 15 20:45:20 2009 +0200 @@ -0,0 +1,82 @@ +/* + * Information on command status left of scrollbar (with panel) + * + * @author Fabian Immler, TU Munich + */ + +package isabelle.jedit + +import isabelle.prover.{Prover, Command} +import isabelle.proofdocument.ProofDocument + +import javax.swing.{JPanel, ToolTipManager} +import java.awt.event.{MouseAdapter, MouseEvent} +import java.awt.{BorderLayout, Graphics, Dimension} + +import org.gjt.sp.jedit.gui.RolloverButton +import org.gjt.sp.jedit.textarea.JEditTextArea +import org.gjt.sp.jedit.buffer.JEditBuffer + + +class Document_Overview( + prover: Prover, + text_area: JEditTextArea, + to_current: (ProofDocument, Int) => Int) + extends JPanel(new BorderLayout) +{ + private val WIDTH = 10 + private val HEIGHT = 2 + + setRequestFocusEnabled(false) + + addMouseListener(new MouseAdapter { + override def mousePressed(event: MouseEvent) { + val line = y_to_line(event.getY) + if (line >= 0 && line < text_area.getLineCount) + text_area.setCaretPosition(text_area.getLineStartOffset(line)) + } + }) + + override def addNotify() { + super.addNotify() + ToolTipManager.sharedInstance.registerComponent(this) + } + + override def removeNotify() { + super.removeNotify + ToolTipManager.sharedInstance.unregisterComponent(this) + } + + override def getToolTipText(event: MouseEvent): String = + { + val buffer = text_area.getBuffer + val lineCount = buffer.getLineCount + val line = y_to_line(event.getY()) + if (line >= 0 && line < text_area.getLineCount) "TODO:
Tooltip" + else "" + } + + override def paintComponent(gfx: Graphics) { + super.paintComponent(gfx) + val buffer = text_area.getBuffer + val theory_view = Isabelle.prover_setup(buffer).get.theory_view + val doc = theory_view.current_document() + + for (command <- doc.commands) { + val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc))) + val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1 + val y = line_to_y(line1) + val height = HEIGHT * (line2 - line1) + gfx.setColor(TheoryView.choose_color(command, doc)) + gfx.fillRect(0, y, getWidth - 1, height) + } + } + + override def getPreferredSize = new Dimension(WIDTH, 0) + + private def line_to_y(line: Int): Int = + (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) + + private def y_to_line(y: Int): Int = + (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight +} \ No newline at end of file