46572
|
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 |
|