|
1 /* |
|
2 * Information on command status left of scrollbar (with panel) |
|
3 * |
|
4 * @author Fabian Immler, TU Munich |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 import isabelle.prover.{Prover, Command} |
|
10 import isabelle.proofdocument.ProofDocument |
|
11 |
|
12 import javax.swing.{JPanel, ToolTipManager} |
|
13 import java.awt.event.{MouseAdapter, MouseEvent} |
|
14 import java.awt.{BorderLayout, Graphics, Dimension} |
|
15 |
|
16 import org.gjt.sp.jedit.gui.RolloverButton |
|
17 import org.gjt.sp.jedit.textarea.JEditTextArea |
|
18 import org.gjt.sp.jedit.buffer.JEditBuffer |
|
19 |
|
20 |
|
21 class Document_Overview( |
|
22 prover: Prover, |
|
23 text_area: JEditTextArea, |
|
24 to_current: (ProofDocument, Int) => Int) |
|
25 extends JPanel(new BorderLayout) |
|
26 { |
|
27 private val WIDTH = 10 |
|
28 private val HEIGHT = 2 |
|
29 |
|
30 setRequestFocusEnabled(false) |
|
31 |
|
32 addMouseListener(new MouseAdapter { |
|
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)) |
|
37 } |
|
38 }) |
|
39 |
|
40 override def addNotify() { |
|
41 super.addNotify() |
|
42 ToolTipManager.sharedInstance.registerComponent(this) |
|
43 } |
|
44 |
|
45 override def removeNotify() { |
|
46 super.removeNotify |
|
47 ToolTipManager.sharedInstance.unregisterComponent(this) |
|
48 } |
|
49 |
|
50 override def getToolTipText(event: MouseEvent): String = |
|
51 { |
|
52 val buffer = text_area.getBuffer |
|
53 val lineCount = buffer.getLineCount |
|
54 val line = y_to_line(event.getY()) |
|
55 if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>" |
|
56 else "" |
|
57 } |
|
58 |
|
59 override def paintComponent(gfx: Graphics) { |
|
60 super.paintComponent(gfx) |
|
61 val buffer = text_area.getBuffer |
|
62 val theory_view = Isabelle.prover_setup(buffer).get.theory_view |
|
63 val doc = theory_view.current_document() |
|
64 |
|
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 } |
|
73 } |
|
74 |
|
75 override def getPreferredSize = new Dimension(WIDTH, 0) |
|
76 |
|
77 private def line_to_y(line: Int): Int = |
|
78 (line * getHeight) / (text_area.getBuffer.getLineCount max text_area.getVisibleLines) |
|
79 |
|
80 private def y_to_line(y: Int): Int = |
|
81 (y * (text_area.getBuffer.getLineCount max text_area.getVisibleLines)) / getHeight |
|
82 } |