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 |
|
|
12 |
|
|
13 |
import org.gjt.sp.jedit.{jEdit, Buffer, View}
|
|
14 |
import org.gjt.sp.jedit.buffer.JEditBuffer
|
|
15 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
|
|
16 |
|
|
17 |
|
|
18 |
object JEdit_Lib
|
|
19 |
{
|
|
20 |
/* buffers */
|
|
21 |
|
|
22 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
|
|
23 |
Swing_Thread.now { buffer_lock(buffer) { body } }
|
|
24 |
|
|
25 |
def buffer_text(buffer: JEditBuffer): String =
|
|
26 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
|
|
27 |
|
|
28 |
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
|
|
29 |
|
|
30 |
def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
|
|
31 |
Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
|
|
32 |
|
|
33 |
def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
|
|
34 |
{
|
|
35 |
val name = buffer_name(buffer)
|
|
36 |
Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
|
|
37 |
}
|
|
38 |
|
|
39 |
|
|
40 |
/* main jEdit components */
|
|
41 |
|
|
42 |
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
|
|
43 |
|
|
44 |
def jedit_buffer(name: String): Option[Buffer] =
|
|
45 |
jedit_buffers().find(buffer => buffer_name(buffer) == name)
|
|
46 |
|
|
47 |
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
|
|
48 |
|
|
49 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
|
|
50 |
view.getEditPanes().iterator.map(_.getTextArea)
|
|
51 |
|
|
52 |
def jedit_text_areas(): Iterator[JEditTextArea] =
|
|
53 |
jedit_views().flatMap(jedit_text_areas(_))
|
|
54 |
|
|
55 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
|
|
56 |
jedit_text_areas().filter(_.getBuffer == buffer)
|
|
57 |
|
|
58 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
|
|
59 |
{
|
|
60 |
try { buffer.readLock(); body }
|
|
61 |
finally { buffer.readUnlock() }
|
|
62 |
}
|
49407
|
63 |
|
|
64 |
|
|
65 |
/* point range */
|
|
66 |
|
|
67 |
def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
|
|
68 |
buffer_lock(buffer) {
|
|
69 |
def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
|
|
70 |
try {
|
|
71 |
val c = text(offset)
|
|
72 |
if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
|
|
73 |
Text.Range(offset, offset + 2)
|
|
74 |
else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
|
|
75 |
Text.Range(offset - 1, offset + 1)
|
|
76 |
else Text.Range(offset, offset + 1)
|
|
77 |
}
|
|
78 |
catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
|
|
79 |
}
|
49406
|
80 |
}
|
|
81 |
|