author | wenzelm |
Tue, 22 Apr 2014 23:49:15 +0200 | |
changeset 56662 | f373fb77e0a4 |
parent 52972 | 8fd8e1c14988 |
child 57612 | 990ffb84489b |
permissions | -rw-r--r-- |
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 |
||
49346 | 14 |
import java.awt.{Graphics, Graphics2D, BorderLayout, Dimension, Color} |
46572 | 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 |
|
50895 | 25 |
private val HEIGHT = 4 |
46572 | 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 |
||
49346 | 51 |
|
52 |
/* painting based on cached result */ |
|
53 |
||
54 |
private var cached_colors: List[(Color, Int, Int)] = Nil |
|
55 |
||
52972 | 56 |
private var last_snapshot = Document.Snapshot.init |
50205 | 57 |
private var last_options = PIDE.options.value |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
58 |
private var last_relevant_range = Text.Range(0) |
49346 | 59 |
private var last_line_count = 0 |
60 |
private var last_char_count = 0 |
|
61 |
private var last_L = 0 |
|
62 |
private var last_H = 0 |
|
63 |
||
46572 | 64 |
override def paintComponent(gfx: Graphics) |
65 |
{ |
|
66 |
super.paintComponent(gfx) |
|
56662
f373fb77e0a4
avoid "Adaptation of argument list by inserting ()" -- deprecated in scala-2.11.0;
wenzelm
parents:
52972
diff
changeset
|
67 |
Swing_Thread.assert {} |
46572 | 68 |
|
49411 | 69 |
doc_view.rich_text_area.robust_body(()) { |
49406 | 70 |
JEdit_Lib.buffer_lock(buffer) { |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
71 |
val rendering = doc_view.get_rendering() |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
72 |
val snapshot = rendering.snapshot |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
73 |
val options = rendering.options |
46572 | 74 |
|
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
75 |
if (snapshot.is_outdated) { |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
76 |
gfx.setColor(rendering.outdated_color) |
49346 | 77 |
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
78 |
} |
|
79 |
else { |
|
80 |
gfx.setColor(getBackground) |
|
81 |
gfx.asInstanceOf[Graphics2D].fill(gfx.getClipBounds) |
|
82 |
||
83 |
val line_count = buffer.getLineCount |
|
84 |
val char_count = buffer.getLength |
|
46572 | 85 |
|
49346 | 86 |
val L = lines() |
87 |
val H = getHeight() |
|
46572 | 88 |
|
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
89 |
val relevant_range = |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
90 |
JEdit_Lib.visible_range(text_area) match { |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
91 |
case None => Text.Range(0) |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
92 |
case Some(visible_range) => |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
93 |
val len = rendering.overview_limit max visible_range.length |
50886
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
94 |
val start = (visible_range.start + visible_range.stop - len) / 2 |
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
95 |
val stop = start + len |
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
96 |
|
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
97 |
if (start < 0) Text.Range(0, len min char_count) |
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
98 |
else if (stop > char_count) Text.Range((char_count - len) max 0, char_count) |
05054cf8ca77
more precise relevant_range to exploit overview_limit better;
wenzelm
parents:
50205
diff
changeset
|
99 |
else Text.Range(start, stop) |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
100 |
} |
49356 | 101 |
|
49346 | 102 |
if (!(line_count == last_line_count && char_count == last_char_count && |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
103 |
L == last_L && H == last_H && relevant_range == last_relevant_range && |
51494 | 104 |
(snapshot eq_content last_snapshot) && (options eq last_options))) |
49346 | 105 |
{ |
106 |
@tailrec def loop(l: Int, h: Int, p: Int, q: Int, colors: List[(Color, Int, Int)]) |
|
107 |
: List[(Color, Int, Int)] = |
|
108 |
{ |
|
109 |
if (l < line_count && h < H) { |
|
110 |
val p1 = p + H |
|
111 |
val q1 = q + HEIGHT * L |
|
112 |
val (l1, h1) = |
|
113 |
if (p1 >= q1) (l + 1, h + (p1 - q) / L) |
|
114 |
else (l + (q1 - p) / H, h + HEIGHT) |
|
46572 | 115 |
|
49346 | 116 |
val start = buffer.getLineStartOffset(l) |
117 |
val end = |
|
118 |
if (l1 < line_count) buffer.getLineStartOffset(l1) |
|
119 |
else char_count |
|
120 |
val range = Text.Range(start, end) |
|
46572 | 121 |
|
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
122 |
val range_color = |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
123 |
if (range overlaps relevant_range) rendering.overview_color(range) |
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
124 |
else Some(rendering.outdated_color) |
49346 | 125 |
val colors1 = |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
126 |
(range_color, colors) match { |
49346 | 127 |
case (Some(color), (old_color, old_h, old_h1) :: rest) |
128 |
if color == old_color && old_h1 == h => (color, old_h, h1) :: rest |
|
129 |
case (Some(color), _) => (color, h, h1) :: colors |
|
130 |
case (None, _) => colors |
|
131 |
} |
|
132 |
loop(l1, h1, p + (l1 - l) * H, q + (h1 - h) * L, colors1) |
|
133 |
} |
|
134 |
else colors.reverse |
|
135 |
} |
|
136 |
cached_colors = loop(0, 0, 0, 0, Nil) |
|
46572 | 137 |
|
49346 | 138 |
last_snapshot = snapshot |
49356 | 139 |
last_options = options |
49969
72216713733a
further attempts to cope with large files via option jedit_text_overview_limit;
wenzelm
parents:
49697
diff
changeset
|
140 |
last_relevant_range = relevant_range |
49346 | 141 |
last_line_count = line_count |
142 |
last_char_count = char_count |
|
143 |
last_L = L |
|
144 |
last_H = H |
|
145 |
} |
|
146 |
||
147 |
for ((color, h, h1) <- cached_colors) { |
|
148 |
gfx.setColor(color) |
|
149 |
gfx.fillRect(0, h, getWidth, h1 - h) |
|
46572 | 150 |
} |
151 |
} |
|
152 |
} |
|
153 |
} |
|
154 |
} |
|
155 |
} |
|
156 |