author | wenzelm |
Tue, 15 Sep 2009 20:46:46 +0200 | |
changeset 34737 | 6c1fa25ca950 |
parent 34736 | src/Tools/jEdit/src/jedit/document_overview.scala@ff7734c8bdb7 |
permissions | -rw-r--r-- |
34408 | 1 |
/* |
34458
e2aa32bb73c0
- renamed Command.Phase to Command.Status (cf. src/Pure/Isar/isar.ML);
wenzelm
parents:
34456
diff
changeset
|
2 |
* Information on command status left of scrollbar (with panel) |
34408 | 3 |
* |
4 |
* @author Fabian Immler, TU Munich |
|
5 |
*/ |
|
6 |
||
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
7 |
package isabelle.jedit |
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
8 |
|
34654 | 9 |
import isabelle.prover.{Prover, Command} |
34554
7dc6c231da40
abs. stops, markup nodes depend on doc-version;
immler@in.tum.de
parents:
34548
diff
changeset
|
10 |
import isabelle.proofdocument.ProofDocument |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
11 |
|
34734 | 12 |
import javax.swing.{JPanel, ToolTipManager} |
13 |
import java.awt.event.{MouseAdapter, MouseEvent} |
|
14 |
import java.awt.{BorderLayout, Graphics, Dimension} |
|
15 |
||
34709 | 16 |
import org.gjt.sp.jedit.gui.RolloverButton |
17 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
|
18 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
|
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
19 |
|
34733 | 20 |
|
34736 | 21 |
class Document_Overview( |
34709 | 22 |
prover: Prover, |
34733 | 23 |
text_area: JEditTextArea, |
34709 | 24 |
to_current: (ProofDocument, Int) => Int) |
25 |
extends JPanel(new BorderLayout) |
|
34654 | 26 |
{ |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
27 |
private val WIDTH = 10 |
34733 | 28 |
private val HEIGHT = 2 |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
29 |
|
34709 | 30 |
setRequestFocusEnabled(false) |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
31 |
|
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
32 |
addMouseListener(new MouseAdapter { |
34733 | 33 |
override def mousePressed(event: MouseEvent) { |
34 |
val line = y_to_line(event.getY) |
|
35 |
if (line >= 0 && line < text_area.getLineCount) |
|
36 |
text_area.setCaretPosition(text_area.getLineStartOffset(line)) |
|
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
37 |
} |
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
38 |
}) |
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
39 |
|
34733 | 40 |
override def addNotify() { |
34709 | 41 |
super.addNotify() |
42 |
ToolTipManager.sharedInstance.registerComponent(this) |
|
34678 | 43 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
44 |
|
34733 | 45 |
override def removeNotify() { |
34678 | 46 |
super.removeNotify |
34709 | 47 |
ToolTipManager.sharedInstance.unregisterComponent(this) |
34678 | 48 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
49 |
|
34733 | 50 |
override def getToolTipText(event: MouseEvent): String = |
34678 | 51 |
{ |
34733 | 52 |
val buffer = text_area.getBuffer |
34678 | 53 |
val lineCount = buffer.getLineCount |
34733 | 54 |
val line = y_to_line(event.getY()) |
34735 | 55 |
if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>" |
34733 | 56 |
else "" |
34678 | 57 |
} |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
58 |
|
34711 | 59 |
override def paintComponent(gfx: Graphics) { |
34678 | 60 |
super.paintComponent(gfx) |
34733 | 61 |
val buffer = text_area.getBuffer |
34650 | 62 |
val theory_view = Isabelle.prover_setup(buffer).get.theory_view |
34734 | 63 |
val doc = theory_view.current_document() |
34678 | 64 |
|
34734 | 65 |
for (command <- doc.commands) { |
66 |
val line1 = buffer.getLineOfOffset(to_current(doc, command.start(doc))) |
|
67 |
val line2 = buffer.getLineOfOffset(to_current(doc, command.stop(doc))) + 1 |
|
68 |
val y = line_to_y(line1) |
|
69 |
val height = HEIGHT * (line2 - line1) |
|
70 |
gfx.setColor(TheoryView.choose_color(command, doc)) |
|
71 |
gfx.fillRect(0, y, getWidth - 1, height) |
|
72 |
} |
|
34678 | 73 |
} |
34513 | 74 |
|
34733 | 75 |
override def getPreferredSize = new Dimension(WIDTH, 0) |
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
76 |
|
34733 | 77 |
private def line_to_y(line: Int): Int = |
78 |
(line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) |
|
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
79 |
|
34733 | 80 |
private def y_to_line(y: Int): Int = |
81 |
(y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight |
|
34403
6c812a3cb170
information on command-phase left of scrollbar (with panel)
immler@in.tum.de
parents:
diff
changeset
|
82 |
} |