author | wenzelm |
Fri, 05 Oct 2012 13:48:22 +0200 | |
changeset 49710 | 21d88a631fcc |
parent 49409 | 7140a738aa49 |
child 49712 | a1bd8fe5131b |
permissions | -rw-r--r-- |
49406 | 1 |
/* Title: Tools/jEdit/src/jedit_lib.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Misc library functions for jEdit. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle.jedit |
|
8 |
||
9 |
||
10 |
import isabelle._ |
|
11 |
||
49710
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
12 |
import java.awt.{Component, Container, Frame} |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
13 |
|
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
14 |
import scala.annotation.tailrec |
49406 | 15 |
|
16 |
import org.gjt.sp.jedit.{jEdit, Buffer, View} |
|
17 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
|
18 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
|
19 |
||
20 |
||
21 |
object JEdit_Lib |
|
22 |
{ |
|
49710
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
23 |
/* frames */ |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
24 |
|
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
25 |
def parent_frame(component: Component): Option[Frame] = |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
26 |
{ |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
27 |
@tailrec def find(c: Container): Option[Frame] = |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
28 |
c match { |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
29 |
case null => None |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
30 |
case frame: Frame => Some(frame) |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
31 |
case _ => find(c.getParent) |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
32 |
} |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
33 |
find(component.getParent) |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
34 |
} |
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
35 |
|
21d88a631fcc
refer to parent frame -- relevant for floating dockables in particular;
wenzelm
parents:
49409
diff
changeset
|
36 |
|
49406 | 37 |
/* buffers */ |
38 |
||
39 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
40 |
Swing_Thread.now { buffer_lock(buffer) { body } } |
|
41 |
||
42 |
def buffer_text(buffer: JEditBuffer): String = |
|
43 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
|
44 |
||
45 |
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
|
46 |
||
47 |
def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = |
|
48 |
Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName)) |
|
49 |
||
50 |
def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = |
|
51 |
{ |
|
52 |
val name = buffer_name(buffer) |
|
53 |
Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) |
|
54 |
} |
|
55 |
||
56 |
||
57 |
/* main jEdit components */ |
|
58 |
||
59 |
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
|
60 |
||
61 |
def jedit_buffer(name: String): Option[Buffer] = |
|
62 |
jedit_buffers().find(buffer => buffer_name(buffer) == name) |
|
63 |
||
64 |
def jedit_views(): Iterator[View] = jEdit.getViews().iterator |
|
65 |
||
66 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
|
67 |
view.getEditPanes().iterator.map(_.getTextArea) |
|
68 |
||
69 |
def jedit_text_areas(): Iterator[JEditTextArea] = |
|
70 |
jedit_views().flatMap(jedit_text_areas(_)) |
|
71 |
||
72 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = |
|
73 |
jedit_text_areas().filter(_.getBuffer == buffer) |
|
74 |
||
75 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
76 |
{ |
|
77 |
try { buffer.readLock(); body } |
|
78 |
finally { buffer.readUnlock() } |
|
79 |
} |
|
49407 | 80 |
|
81 |
||
82 |
/* point range */ |
|
83 |
||
84 |
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range = |
|
85 |
buffer_lock(buffer) { |
|
86 |
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0) |
|
87 |
try { |
|
88 |
val c = text(offset) |
|
89 |
if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1))) |
|
90 |
Text.Range(offset, offset + 2) |
|
91 |
else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1))) |
|
92 |
Text.Range(offset - 1, offset + 1) |
|
93 |
else Text.Range(offset, offset + 1) |
|
94 |
} |
|
95 |
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) } |
|
96 |
} |
|
49408 | 97 |
|
98 |
||
99 |
/* proper line range */ |
|
100 |
||
101 |
// NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength |
|
102 |
def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range = |
|
103 |
Text.Range(start, end min buffer.getLength) |
|
104 |
||
105 |
||
106 |
/* visible text range */ |
|
107 |
||
108 |
def visible_range(text_area: TextArea): Option[Text.Range] = |
|
109 |
{ |
|
110 |
val buffer = text_area.getBuffer |
|
111 |
val n = text_area.getVisibleLines |
|
112 |
if (n > 0) { |
|
113 |
val start = text_area.getScreenLineStartOffset(0) |
|
114 |
val raw_end = text_area.getScreenLineEndOffset(n - 1) |
|
115 |
Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength)) |
|
116 |
} |
|
117 |
else None |
|
118 |
} |
|
119 |
||
120 |
def invalidate_range(text_area: TextArea, range: Text.Range) |
|
121 |
{ |
|
122 |
val buffer = text_area.getBuffer |
|
123 |
text_area.invalidateLineRange( |
|
124 |
buffer.getLineOfOffset(range.start), |
|
125 |
buffer.getLineOfOffset(range.stop)) |
|
126 |
} |
|
49409 | 127 |
|
128 |
||
129 |
/* char width */ |
|
130 |
||
131 |
def char_width(text_area: TextArea): Int = |
|
132 |
{ |
|
133 |
val painter = text_area.getPainter |
|
134 |
val font = painter.getFont |
|
135 |
val font_context = painter.getFontRenderContext |
|
136 |
font.getStringBounds(" ", font_context).getWidth.round.toInt |
|
137 |
} |
|
138 |
||
139 |
||
140 |
/* graphics range */ |
|
141 |
||
142 |
class Gfx_Range(val x: Int, val y: Int, val length: Int) |
|
143 |
||
144 |
// NB: jEdit already normalizes \r\n and \r to \n |
|
145 |
// NB: last line lacks \n |
|
146 |
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
147 |
{ |
|
148 |
val buffer = text_area.getBuffer |
|
149 |
||
150 |
val p = text_area.offsetToXY(range.start) |
|
151 |
||
152 |
val end = buffer.getLength |
|
153 |
val stop = range.stop |
|
154 |
val (q, r) = |
|
155 |
if (stop >= end) (text_area.offsetToXY(end), char_width(text_area)) |
|
156 |
else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n") |
|
157 |
(text_area.offsetToXY(stop - 1), char_width(text_area)) |
|
158 |
else (text_area.offsetToXY(stop), 0) |
|
159 |
||
160 |
if (p != null && q != null && p.x < q.x + r && p.y == q.y) |
|
161 |
Some(new Gfx_Range(p.x, p.y, q.x + r - p.x)) |
|
162 |
else None |
|
163 |
} |
|
49406 | 164 |
} |
165 |