|
1 /* Title: Tools/jEdit/src/text_overview.scala |
|
2 Author: Makarius |
|
3 |
|
4 Swing component for text status overview. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import scala.annotation.tailrec |
|
13 |
|
14 import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension} |
|
15 import java.awt.event.{MouseAdapter, MouseEvent} |
|
16 import javax.swing.{JPanel, ToolTipManager} |
|
17 |
|
18 |
|
19 class Text_Overview(doc_view: Document_View) extends JPanel(new BorderLayout) |
|
20 { |
|
21 private val text_area = doc_view.text_area |
|
22 private val buffer = doc_view.model.buffer |
|
23 |
|
24 private val WIDTH = 10 |
|
25 private val HEIGHT = 2 |
|
26 |
|
27 private def lines(): Int = buffer.getLineCount max text_area.getVisibleLines |
|
28 |
|
29 setPreferredSize(new Dimension(WIDTH, 0)) |
|
30 |
|
31 setRequestFocusEnabled(false) |
|
32 |
|
33 addMouseListener(new MouseAdapter { |
|
34 override def mousePressed(event: MouseEvent) { |
|
35 val line = (event.getY * lines()) / getHeight |
|
36 if (line >= 0 && line < text_area.getLineCount) |
|
37 text_area.setCaretPosition(text_area.getLineStartOffset(line)) |
|
38 } |
|
39 }) |
|
40 |
|
41 override def addNotify() { |
|
42 super.addNotify() |
|
43 ToolTipManager.sharedInstance.registerComponent(this) |
|
44 } |
|
45 |
|
46 override def removeNotify() { |
|
47 ToolTipManager.sharedInstance.unregisterComponent(this) |
|
48 super.removeNotify |
|
49 } |
|
50 |
|
51 override def paintComponent(gfx: Graphics) |
|
52 { |
|
53 super.paintComponent(gfx) |
|
54 Swing_Thread.assert() |
|
55 |
|
56 doc_view.robust_body(()) { |
|
57 Isabelle.buffer_lock(buffer) { |
|
58 val snapshot = doc_view.update_snapshot() |
|
59 |
|
60 gfx.setColor(getBackground) |
|
61 gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
|
62 |
|
63 val line_count = buffer.getLineCount |
|
64 val char_count = buffer.getLength |
|
65 |
|
66 val L = lines() |
|
67 val H = getHeight() |
|
68 |
|
69 @tailrec def paint_loop(l: Int, h: Int, p: Int, q: Int): Unit = |
|
70 { |
|
71 if (l < line_count && h < H) { |
|
72 val p1 = p + H |
|
73 val q1 = q + HEIGHT * L |
|
74 val (l1, h1) = |
|
75 if (p1 >= q1) (l + 1, h + (p1 - q) / L) |
|
76 else (l + (q1 - p) / H, h + HEIGHT) |
|
77 |
|
78 val start = buffer.getLineStartOffset(l) |
|
79 val end = |
|
80 if (l1 < line_count) buffer.getLineStartOffset(l1) |
|
81 else char_count |
|
82 |
|
83 Isabelle_Rendering.overview_color(snapshot, Text.Range(start, end)) match { |
|
84 case None => |
|
85 case Some(color) => |
|
86 gfx.setColor(color) |
|
87 gfx.fillRect(0, h, getWidth, h1 - h) |
|
88 } |
|
89 paint_loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L) |
|
90 } |
|
91 } |
|
92 paint_loop(0, 0, 0, 0) |
|
93 } |
|
94 } |
|
95 } |
|
96 } |
|
97 |