author | wenzelm |
Mon, 12 Aug 2013 14:53:16 +0200 | |
changeset 52978 | 37fbb3fde380 |
parent 52977 | 15254e32d299 |
child 52980 | 28f59ca8ce78 |
permissions | -rw-r--r-- |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/jedit_editor.scala |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
3 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
4 |
PIDE editor operations for jEdit. |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
5 |
*/ |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
6 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
8 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
9 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
11 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
12 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
13 |
import org.gjt.sp.jedit.{jEdit, View} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
14 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
15 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
16 |
class JEdit_Editor extends Editor[View] |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
17 |
{ |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
18 |
/* session */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
19 |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
20 |
def session: Session = PIDE.session |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
21 |
|
52974 | 22 |
def flush() |
23 |
{ |
|
24 |
Swing_Thread.require() |
|
25 |
||
26 |
session.update( |
|
27 |
(List.empty[Document.Edit_Text] /: JEdit_Lib.jedit_buffers().toList) { |
|
28 |
case (edits, buffer) => |
|
29 |
JEdit_Lib.buffer_lock(buffer) { |
|
30 |
PIDE.document_model(buffer) match { |
|
31 |
case Some(model) => model.flushed_edits() ::: edits |
|
32 |
case None => edits |
|
33 |
} |
|
34 |
} |
|
35 |
} |
|
36 |
) |
|
37 |
} |
|
38 |
||
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
39 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
40 |
/* current situation */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
41 |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
42 |
def current_context: View = |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
43 |
Swing_Thread.require { jEdit.getActiveView() } |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
44 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
45 |
def current_node(view: View): Option[Document.Node.Name] = |
52973 | 46 |
Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
47 |
|
52978 | 48 |
def current_node_snapshot(view: View): Option[Document.Snapshot] = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
49 |
Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
50 |
|
52974 | 51 |
def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
52 |
{ |
|
53 |
Swing_Thread.require() |
|
54 |
||
55 |
JEdit_Lib.jedit_buffer(name.node) match { |
|
56 |
case Some(buffer) => |
|
57 |
PIDE.document_model(buffer) match { |
|
58 |
case Some(model) => model.snapshot |
|
59 |
case None => session.snapshot(name) |
|
60 |
} |
|
61 |
case None => session.snapshot(name) |
|
62 |
} |
|
63 |
} |
|
64 |
||
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
65 |
def current_command(view: View, snapshot: Document.Snapshot): Option[(Command, Text.Offset)] = |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
66 |
{ |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
67 |
Swing_Thread.require() |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
68 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
69 |
if (snapshot.is_outdated) None |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
70 |
else { |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
71 |
val text_area = view.getTextArea |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
72 |
PIDE.document_view(text_area) match { |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
73 |
case Some(doc_view) => |
52973 | 74 |
val node = snapshot.version.nodes(doc_view.model.node_name) |
52978 | 75 |
val caret_commands = node.command_range(text_area.getCaretPosition) |
76 |
if (caret_commands.hasNext) Some(caret_commands.next) else None |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
77 |
case None => None |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
78 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
79 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
80 |
} |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
81 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
82 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
83 |
/* overlays */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
84 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
85 |
private var overlays = Document.Overlays.empty |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
86 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
87 |
def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
88 |
synchronized { overlays(name) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
89 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
90 |
def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
91 |
synchronized { overlays = overlays.insert(command, fn, args) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
92 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
93 |
def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
94 |
synchronized { overlays = overlays.remove(command, fn, args) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
95 |
} |