--- 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) "<html><b>TODO:</b><br>Tooltip</html>"
- 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
--- 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)
--- /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) "<html><b>TODO:</b><br>Tooltip</html>"
+ 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