author | wenzelm |
Mon, 13 Jun 2011 12:29:26 +0200 | |
changeset 43372 | 2df2144b0910 |
parent 43371 | 98de43fc9733 |
child 43373 | 639c3aca2ed3 |
permissions | -rw-r--r-- |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/text_painter.scala |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
3 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
4 |
Replacement painter for jEdit text area. |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
6 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
8 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
9 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
11 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
12 |
import java.awt.{Graphics, Graphics2D} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
13 |
import java.util.ArrayList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
14 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
15 |
import org.gjt.sp.jedit.Debug |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
16 |
import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
17 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
18 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
19 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
20 |
class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
21 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
22 |
private val orig_text_painter: TextAreaExtension = |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
23 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
24 |
val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText" |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
25 |
text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
26 |
match { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
27 |
case List(x) => x |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
28 |
case _ => error("Expected exactly one " + name) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
29 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
30 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
31 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
32 |
var use = false |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
33 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
34 |
override def paintScreenLineRange(gfx: Graphics2D, |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
35 |
first_line: Int, last_line: Int, physical_lines: Array[Int], |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
36 |
start: Array[Int], end: Array[Int], y: Int, line_height: Int) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
37 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
38 |
if (use) { |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
39 |
val buffer = text_area.getBuffer |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
40 |
Isabelle.swing_buffer_lock(buffer) { |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
41 |
val painter = text_area.getPainter |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
42 |
val font = painter.getFont |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
43 |
val font_context = painter.getFontRenderContext |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
44 |
val fm = painter.getFontMetrics |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
45 |
|
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
46 |
// see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged |
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
47 |
// see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
48 |
val char_width = font.getStringBounds(" ", font_context).getWidth.round.toInt |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
49 |
val soft_wrap = buffer.getStringProperty("wrap") == "soft" |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
50 |
val wrap_margin = |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
51 |
{ |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
52 |
val max = buffer.getIntegerProperty("maxLineLen", 0) |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
53 |
if (max > 0) font.getStringBounds(" " * max, font_context).getWidth.toInt |
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
54 |
else if (soft_wrap) painter.getWidth - char_width * 3 |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
55 |
else 0 |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
56 |
}.toFloat |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
57 |
|
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
58 |
val line_infos: Map[Text.Offset, Chunk] = |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
59 |
{ |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
60 |
val out = new ArrayList[Chunk] |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
61 |
val handler = new DisplayTokenHandler |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
62 |
val margin = if (soft_wrap) wrap_margin else 0.0f |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
63 |
|
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
64 |
var result = Map[Text.Offset, Chunk]() |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
65 |
for (line <- physical_lines.iterator.filter(i => i != -1)) { |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
66 |
out.clear |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
67 |
handler.init(painter.getStyles, font_context, painter, out, margin) |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
68 |
buffer.markTokens(line, handler) |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
69 |
|
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
70 |
val line_start = buffer.getLineStartOffset(line) |
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
71 |
for (i <- 0 until out.size) { |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
72 |
val chunk = out.get(i) |
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
73 |
result += (line_start + chunk.offset -> chunk) |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
74 |
} |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
75 |
} |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
76 |
result |
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
77 |
} |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
78 |
|
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
79 |
val clip = gfx.getClip |
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
80 |
val x0 = text_area.getHorizontalOffset |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
81 |
var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
82 |
for (i <- 0 until physical_lines.length) { |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
83 |
if (physical_lines(i) != -1) { |
43371
98de43fc9733
more precise imitation of original TextAreaPainter$PaintText;
wenzelm
parents:
43370
diff
changeset
|
84 |
line_infos.get(start(i)) match { |
43372
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
85 |
case Some(chunk) => |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
86 |
val w = Chunk.paintChunkList(chunk, gfx, x0, y0, !Debug.DISABLE_GLYPH_VECTOR).toInt |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
87 |
gfx.setFont(font) |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
88 |
gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE) |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
89 |
orig_text_painter.paintValidLine( |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
90 |
gfx, first_line + i, physical_lines(i), start(i), end(i), y + line_height * i) |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
91 |
gfx.setClip(clip) |
2df2144b0910
use orig_text_painter for extras outside main text (also required to update internal line infos);
wenzelm
parents:
43371
diff
changeset
|
92 |
|
43369
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
93 |
case None => |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
94 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
95 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
96 |
y0 += line_height |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
97 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
98 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
99 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
100 |
else |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
101 |
orig_text_painter.paintScreenLineRange( |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
102 |
gfx, first_line, last_line, physical_lines, start, end, y, line_height) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
103 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
104 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
105 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
106 |
/* activation */ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
107 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
108 |
def activate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
109 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
110 |
val painter = text_area.getPainter |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
111 |
painter.removeExtension(orig_text_painter) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
112 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, this) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
113 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
114 |
|
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
115 |
def deactivate() |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
116 |
{ |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
117 |
val painter = text_area.getPainter |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
118 |
painter.removeExtension(this) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
119 |
painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter) |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
120 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
121 |
} |
4c86b3405010
separate isabelle.jedit.Text_Painter, which actually replaces the original TextAreaPainter$PaintText instance;
wenzelm
parents:
diff
changeset
|
122 |