|
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 } |
|
63 } |
|
64 |