author | wenzelm |
Mon, 09 Dec 2013 12:16:52 +0100 | |
changeset 54702 | 3daeba5130f0 |
parent 54531 | 8330faaeebd5 |
child 54706 | d3c656f0b7ab |
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 |
||
54522 | 26 |
val edits = PIDE.document_models().flatMap(_.flushed_edits()) |
27 |
if (!edits.isEmpty) session.update(PIDE.document_blobs(), edits) |
|
52974 | 28 |
} |
29 |
||
54461 | 30 |
private val delay_flush = |
31 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
|
32 |
||
33 |
def invoke(): Unit = Swing_Thread.require { delay_flush.invoke() } |
|
34 |
||
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
35 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
36 |
/* current situation */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
37 |
|
52980 | 38 |
override def current_context: View = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
39 |
Swing_Thread.require { jEdit.getActiveView() } |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
40 |
|
52980 | 41 |
override def current_node(view: View): Option[Document.Node.Name] = |
52973 | 42 |
Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
43 |
|
52980 | 44 |
override def current_node_snapshot(view: View): Option[Document.Snapshot] = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
45 |
Swing_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
46 |
|
52980 | 47 |
override def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
52974 | 48 |
{ |
49 |
Swing_Thread.require() |
|
50 |
||
51 |
JEdit_Lib.jedit_buffer(name.node) match { |
|
52 |
case Some(buffer) => |
|
53 |
PIDE.document_model(buffer) match { |
|
54 |
case Some(model) => model.snapshot |
|
55 |
case None => session.snapshot(name) |
|
56 |
} |
|
57 |
case None => session.snapshot(name) |
|
58 |
} |
|
59 |
} |
|
60 |
||
53844
71f103629327
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents:
52980
diff
changeset
|
61 |
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
62 |
{ |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
63 |
Swing_Thread.require() |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
64 |
|
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
65 |
val text_area = view.getTextArea |
54528 | 66 |
val buffer = view.getBuffer |
67 |
||
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
68 |
PIDE.document_view(text_area) match { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
69 |
case Some(doc_view) => |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
70 |
val node = snapshot.version.nodes(doc_view.model.node_name) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
71 |
val caret = snapshot.revert(text_area.getCaretPosition) |
54528 | 72 |
if (caret < buffer.getLength) { |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
73 |
val caret_commands = node.command_range(caret) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
74 |
if (caret_commands.hasNext) { |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
75 |
val (cmd0, _) = caret_commands.next |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
76 |
node.commands.reverse.iterator(cmd0).find(cmd => !cmd.is_ignored) |
53844
71f103629327
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents:
52980
diff
changeset
|
77 |
} |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
78 |
else None |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
79 |
} |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
80 |
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
54528 | 81 |
case None => |
82 |
PIDE.document_model(buffer) match { |
|
54531
8330faaeebd5
restrict node_required status and Theories panel to actual theories;
wenzelm
parents:
54528
diff
changeset
|
83 |
case Some(model) if !model.is_theory => |
54528 | 84 |
snapshot.version.nodes.thy_load_commands(model.node_name) match { |
85 |
case cmd :: _ => Some(cmd) |
|
86 |
case Nil => None |
|
87 |
} |
|
88 |
case _ => None |
|
89 |
} |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
90 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
91 |
} |
52977
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 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
94 |
/* overlays */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
95 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
96 |
private var overlays = Document.Overlays.empty |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
97 |
|
52980 | 98 |
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
|
99 |
synchronized { overlays(name) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
100 |
|
52980 | 101 |
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
|
102 |
synchronized { overlays = overlays.insert(command, fn, args) } |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
103 |
|
52980 | 104 |
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
|
105 |
synchronized { overlays = overlays.remove(command, fn, args) } |
52980 | 106 |
|
107 |
||
108 |
/* hyperlinks */ |
|
109 |
||
110 |
def goto(view: View, file_name: String, line: Int = 0, column: Int = 0) |
|
111 |
{ |
|
112 |
Swing_Thread.require() |
|
113 |
||
114 |
JEdit_Lib.jedit_buffer(file_name) match { |
|
115 |
case Some(buffer) => |
|
116 |
view.goToBuffer(buffer) |
|
117 |
val text_area = view.getTextArea |
|
118 |
||
119 |
try { |
|
120 |
val line_start = text_area.getBuffer.getLineStartOffset(line - 1) |
|
121 |
text_area.moveCaretPosition(line_start) |
|
122 |
if (column > 0) text_area.moveCaretPosition(line_start + column - 1) |
|
123 |
} |
|
124 |
catch { |
|
125 |
case _: ArrayIndexOutOfBoundsException => |
|
126 |
case _: IllegalArgumentException => |
|
127 |
} |
|
128 |
||
129 |
case None => |
|
130 |
val args = |
|
131 |
if (line <= 0) Array(file_name) |
|
132 |
else if (column <= 0) Array(file_name, "+line:" + line.toInt) |
|
133 |
else Array(file_name, "+line:" + line.toInt + "," + column.toInt) |
|
134 |
jEdit.openFiles(view, null, args) |
|
135 |
} |
|
136 |
} |
|
137 |
||
54702
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
138 |
override def hyperlink_url(name: String): Hyperlink = |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
139 |
new Hyperlink { |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
140 |
def follow(view: View) = |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
141 |
default_thread_pool.submit(() => |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
142 |
try { Isabelle_System.open(name) } |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
143 |
catch { |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
144 |
case exn: Throwable => |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
145 |
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
146 |
}) |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
147 |
} |
3daeba5130f0
added document antiquotation @{url}, which produces formal markup for LaTeX and PIDE;
wenzelm
parents:
54531
diff
changeset
|
148 |
|
52980 | 149 |
override def hyperlink_file(file_name: String, line: Int = 0, column: Int = 0): Hyperlink = |
150 |
new Hyperlink { def follow(view: View) = goto(view, file_name, line, column) } |
|
151 |
||
152 |
override def hyperlink_command(snapshot: Document.Snapshot, command: Command, offset: Int = 0) |
|
153 |
: Option[Hyperlink] = |
|
154 |
{ |
|
155 |
if (snapshot.is_outdated) None |
|
156 |
else { |
|
157 |
snapshot.state.find_command(snapshot.version, command.id) match { |
|
158 |
case None => None |
|
159 |
case Some((node, _)) => |
|
160 |
val file_name = command.node_name.node |
|
161 |
val sources = |
|
162 |
node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
|
163 |
(if (offset == 0) Iterator.empty |
|
164 |
else Iterator.single(command.source(Text.Range(0, command.decode(offset))))) |
|
165 |
val (line, column) = ((1, 1) /: sources)(Symbol.advance_line_column) |
|
166 |
Some(new Hyperlink { def follow(view: View) { goto(view, file_name, line, column) } }) |
|
167 |
} |
|
168 |
} |
|
169 |
} |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
170 |
} |