author | wenzelm |
Mon, 12 Aug 2013 17:11:27 +0200 | |
changeset 52980 | 28f59ca8ce78 |
parent 52978 | 37fbb3fde380 |
child 53844 | 71f103629327 |
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 |
|
52980 | 20 |
override def session: Session = PIDE.session |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
21 |
|
52980 | 22 |
override def flush() |
52974 | 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 |
|
52980 | 42 |
override def current_context: View = |
52971
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 |
|
52980 | 45 |
override 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 |
|
52980 | 48 |
override 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 |
|
52980 | 51 |
override def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
52974 | 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 |
||
52980 | 65 |
override def current_command(view: View, snapshot: Document.Snapshot) |
66 |
: Option[(Command, Text.Offset)] = |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
67 |
{ |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
68 |
Swing_Thread.require() |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
69 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
70 |
if (snapshot.is_outdated) None |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
71 |
else { |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
72 |
val text_area = view.getTextArea |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
73 |
PIDE.document_view(text_area) match { |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
74 |
case Some(doc_view) => |
52973 | 75 |
val node = snapshot.version.nodes(doc_view.model.node_name) |
52978 | 76 |
val caret_commands = node.command_range(text_area.getCaretPosition) |
77 |
if (caret_commands.hasNext) Some(caret_commands.next) else None |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
78 |
case None => None |
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 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
81 |
} |
52977
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 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
84 |
/* overlays */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
85 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
86 |
private var overlays = Document.Overlays.empty |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
87 |
|
52980 | 88 |
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
89 |
synchronized { overlays(name) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
90 |
|
52980 | 91 |
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
92 |
synchronized { overlays = overlays.insert(command, fn, args) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
93 |
|
52980 | 94 |
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
95 |
synchronized { overlays = overlays.remove(command, fn, args) } |
52980 | 96 |
|
97 |
||
98 |
/* hyperlinks */ |
|
99 |
||
100 |
def goto(view: View, file_name: String, line: Int = 0, column: Int = 0) |
|
101 |
{ |
|
102 |
Swing_Thread.require() |
|
103 |
||
104 |
JEdit_Lib.jedit_buffer(file_name) match { |
|
105 |
case Some(buffer) => |
|
106 |
view.goToBuffer(buffer) |
|
107 |
val text_area = view.getTextArea |
|
108 |
||
109 |
try { |
|
110 |
val line_start = text_area.getBuffer.getLineStartOffset(line - 1) |
|
111 |
text_area.moveCaretPosition(line_start) |
|
112 |
if (column > 0) text_area.moveCaretPosition(line_start + column - 1) |
|
113 |
} |
|
114 |
catch { |
|
115 |
case _: ArrayIndexOutOfBoundsException => |
|
116 |
case _: IllegalArgumentException => |
|
117 |
} |
|
118 |
||
119 |
case None => |
|
120 |
val args = |
|
121 |
if (line <= 0) Array(file_name) |
|
122 |
else if (column <= 0) Array(file_name, "+line:" + line.toInt) |
|
123 |
else Array(file_name, "+line:" + line.toInt + "," + column.toInt) |
|
124 |
jEdit.openFiles(view, null, args) |
|
125 |
} |
|
126 |
} |
|
127 |
||
128 |
override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink = |
|
129 |
new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) } |
|
130 |
||
131 |
override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0) |
|
132 |
: Option[Hyperlink] = |
|
133 |
{ |
|
134 |
if (snapshot.is_outdated) None |
|
135 |
else { |
|
136 |
snapshot.state.find_command(snapshot.version, command.id) match { |
|
137 |
case None => None |
|
138 |
case Some((node, _)) => |
|
139 |
val file_name = command.node_name.node |
|
140 |
val sources = |
|
141 |
node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
|
142 |
(if (offset == 0) Iterator.empty |
|
143 |
else Iterator.single(command.source(Text.Range(0, command.decode(offset))))) |
|
144 |
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
|
145 |
Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } }) |
|
146 |
} |
|
147 |
} |
|
148 |
} |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
149 |
} |