author | wenzelm |
Wed, 27 Jan 2016 14:14:06 +0100 | |
changeset 62248 | dca0bac351b2 |
parent 62062 | ee610059b0e9 |
child 64521 | 1aef5a0e18d7 |
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 |
|
54706 | 13 |
import java.io.{File => JFile} |
14 |
||
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
15 |
import org.gjt.sp.jedit.{jEdit, View, Buffer} |
54706 | 16 |
import org.gjt.sp.jedit.browser.VFSBrowser |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
17 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
18 |
|
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
19 |
class JEdit_Editor extends Editor[View] |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
20 |
{ |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
21 |
/* session */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
22 |
|
52980 | 23 |
override def session: Session = PIDE.session |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
24 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
25 |
// owned by GUI thread |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
26 |
private var removed_nodes = Set.empty[Document.Node.Name] |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
27 |
|
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
28 |
def remove_node(name: Document.Node.Name): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
29 |
GUI_Thread.require { removed_nodes += name } |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
30 |
|
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61660
diff
changeset
|
31 |
override def flush(hidden: Boolean = false) |
52974 | 32 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
33 |
GUI_Thread.require {} |
52974 | 34 |
|
55783 | 35 |
val doc_blobs = PIDE.document_blobs() |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
36 |
val models = PIDE.document_models() |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
37 |
|
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
38 |
val removed = removed_nodes; removed_nodes = Set.empty |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
39 |
val removed_perspective = |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
40 |
(removed -- models.iterator.map(_.node_name)).toList.map( |
57615
df1b3452d71c
more explicit discrimination of empty nodes -- suppress from Theories panel;
wenzelm
parents:
57612
diff
changeset
|
41 |
name => (name, Document.Node.no_perspective_text)) |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
56770
diff
changeset
|
42 |
|
61728
5f5ff1eab407
double flush to ensure persistent "state" output is reset;
wenzelm
parents:
61660
diff
changeset
|
43 |
val edits = models.flatMap(_.flushed_edits(hidden, doc_blobs)) ::: removed_perspective |
61544 | 44 |
session.update(doc_blobs, edits) |
52974 | 45 |
} |
46 |
||
54461 | 47 |
private val delay_flush = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
48 |
GUI_Thread.delay_last(PIDE.options.seconds("editor_input_delay")) { flush() } |
54461 | 49 |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56729
diff
changeset
|
50 |
def invoke(): Unit = delay_flush.invoke() |
54461 | 51 |
|
60933
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
52 |
def stable_tip_version(): Option[Document.Version] = |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
53 |
GUI_Thread.require { |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
54 |
if (removed_nodes.isEmpty && PIDE.document_models().forall(_.is_stable)) |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
55 |
session.current_state().stable_tip_version |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
56 |
else None |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
57 |
} |
6d03e05ef041
more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;
wenzelm
parents:
60893
diff
changeset
|
58 |
|
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
59 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
60 |
/* current situation */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
61 |
|
52980 | 62 |
override def current_context: View = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
63 |
GUI_Thread.require { jEdit.getActiveView() } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
64 |
|
52980 | 65 |
override def current_node(view: View): Option[Document.Node.Name] = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
66 |
GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.node_name) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
67 |
|
52980 | 68 |
override def current_node_snapshot(view: View): Option[Document.Snapshot] = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
69 |
GUI_Thread.require { PIDE.document_model(view.getBuffer).map(_.snapshot()) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
70 |
|
52980 | 71 |
override def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
52974 | 72 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
73 |
GUI_Thread.require {} |
52974 | 74 |
|
56457
eea4bbe15745
tuned signature -- prefer static type Document.Node.Name;
wenzelm
parents:
56413
diff
changeset
|
75 |
JEdit_Lib.jedit_buffer(name) match { |
52974 | 76 |
case Some(buffer) => |
77 |
PIDE.document_model(buffer) match { |
|
78 |
case Some(model) => model.snapshot |
|
79 |
case None => session.snapshot(name) |
|
80 |
} |
|
81 |
case None => session.snapshot(name) |
|
82 |
} |
|
83 |
} |
|
84 |
||
53844
71f103629327
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents:
52980
diff
changeset
|
85 |
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
86 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
87 |
GUI_Thread.require {} |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
88 |
|
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
89 |
val text_area = view.getTextArea |
54528 | 90 |
val buffer = view.getBuffer |
91 |
||
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
92 |
PIDE.document_view(text_area) match { |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54706
diff
changeset
|
93 |
case Some(doc_view) if doc_view.model.is_theory => |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
94 |
val node = snapshot.version.nodes(doc_view.model.node_name) |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
95 |
val caret = snapshot.revert(text_area.getCaretPosition) |
54528 | 96 |
if (caret < buffer.getLength) { |
56373
0605d90be6fc
tuned signature -- more explicit iterator terminology;
wenzelm
parents:
56314
diff
changeset
|
97 |
val caret_command_iterator = node.command_iterator(caret) |
0605d90be6fc
tuned signature -- more explicit iterator terminology;
wenzelm
parents:
56314
diff
changeset
|
98 |
if (caret_command_iterator.hasNext) { |
0605d90be6fc
tuned signature -- more explicit iterator terminology;
wenzelm
parents:
56314
diff
changeset
|
99 |
val (cmd0, _) = caret_command_iterator.next |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
100 |
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
|
101 |
} |
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
102 |
else None |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
103 |
} |
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
104 |
else node.commands.reverse.iterator.find(cmd => !cmd.is_ignored) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54706
diff
changeset
|
105 |
case _ => |
54528 | 106 |
PIDE.document_model(buffer) match { |
54531
8330faaeebd5
restrict node_required status and Theories panel to actual theories;
wenzelm
parents:
54528
diff
changeset
|
107 |
case Some(model) if !model.is_theory => |
56314 | 108 |
snapshot.version.nodes.load_commands(model.node_name) match { |
54528 | 109 |
case cmd :: _ => Some(cmd) |
110 |
case Nil => None |
|
111 |
} |
|
112 |
case _ => None |
|
113 |
} |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
114 |
} |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
115 |
} |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
116 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
117 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
118 |
/* overlays */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
119 |
|
57873 | 120 |
private val overlays = Synchronized(Document.Overlays.empty) |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
121 |
|
52980 | 122 |
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
57873 | 123 |
overlays.value(name) |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
124 |
|
52980 | 125 |
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
57873 | 126 |
overlays.change(_.insert(command, fn, args)) |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
127 |
|
52980 | 128 |
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
57873 | 129 |
overlays.change(_.remove(command, fn, args)) |
52980 | 130 |
|
131 |
||
55877 | 132 |
/* navigation */ |
52980 | 133 |
|
56413 | 134 |
def push_position(view: View) |
135 |
{ |
|
136 |
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin") |
|
137 |
if (navigator != null) { |
|
59080
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
58545
diff
changeset
|
138 |
try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) } |
56413 | 139 |
catch { case _: NoSuchMethodException => } |
140 |
} |
|
141 |
} |
|
142 |
||
60893 | 143 |
def goto_buffer(focus: Boolean, view: View, buffer: Buffer, offset: Text.Offset) |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
144 |
{ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
145 |
GUI_Thread.require {} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
146 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
147 |
push_position(view) |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
148 |
|
60893 | 149 |
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
150 |
try { view.getTextArea.moveCaretPosition(offset) } |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
151 |
catch { |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
152 |
case _: ArrayIndexOutOfBoundsException => |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
153 |
case _: IllegalArgumentException => |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
154 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
155 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
156 |
|
60893 | 157 |
def goto_file(focus: Boolean, view: View, name: String, line: Int = 0, column: Int = 0) |
52980 | 158 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
159 |
GUI_Thread.require {} |
52980 | 160 |
|
56413 | 161 |
push_position(view) |
162 |
||
54706 | 163 |
JEdit_Lib.jedit_buffer(name) match { |
52980 | 164 |
case Some(buffer) => |
60893 | 165 |
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) |
52980 | 166 |
val text_area = view.getTextArea |
167 |
||
168 |
try { |
|
169 |
val line_start = text_area.getBuffer.getLineStartOffset(line - 1) |
|
170 |
text_area.moveCaretPosition(line_start) |
|
171 |
if (column > 0) text_area.moveCaretPosition(line_start + column - 1) |
|
172 |
} |
|
173 |
catch { |
|
174 |
case _: ArrayIndexOutOfBoundsException => |
|
175 |
case _: IllegalArgumentException => |
|
176 |
} |
|
177 |
||
54706 | 178 |
case None if (new JFile(name)).isDirectory => |
179 |
VFSBrowser.browseDirectory(view, name) |
|
180 |
||
52980 | 181 |
case None => |
182 |
val args = |
|
54706 | 183 |
if (line <= 0) Array(name) |
184 |
else if (column <= 0) Array(name, "+line:" + line.toInt) |
|
185 |
else Array(name, "+line:" + line.toInt + "," + column.toInt) |
|
52980 | 186 |
jEdit.openFiles(view, null, args) |
187 |
} |
|
188 |
} |
|
189 |
||
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
190 |
def goto_doc(view: View, path: Path) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
191 |
{ |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
192 |
if (path.is_file) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
193 |
goto_file(true, view, File.platform_path(path)) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
194 |
else { |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
195 |
Standard_Thread.fork("documentation") { |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
196 |
try { Doc.view(path) } |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
197 |
catch { |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
198 |
case exn: Throwable => |
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
199 |
GUI_Thread.later { |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
200 |
GUI.error_dialog(view, |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
201 |
"Documentation error", GUI.scrollable_text(Exn.message(exn))) |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
202 |
} |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
203 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
204 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
205 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
206 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
207 |
|
55877 | 208 |
|
209 |
/* hyperlinks */ |
|
210 |
||
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
211 |
def hyperlink_doc(name: String): Option[Hyperlink] = |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
212 |
Doc.contents().collectFirst({ |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
213 |
case doc: Doc.Text_File if doc.name == name => doc.path |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
214 |
case doc: Doc.Doc if doc.name == name => doc.path}).map(path => |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
215 |
new Hyperlink { |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
216 |
val external = !path.is_file |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
217 |
def follow(view: View): Unit = goto_doc(view, path) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
218 |
override def toString: String = "doc " + quote(name) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
219 |
}) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
220 |
|
56461 | 221 |
def hyperlink_url(name: String): Hyperlink = |
222 |
new Hyperlink { |
|
56494
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56462
diff
changeset
|
223 |
val external = true |
56729 | 224 |
def follow(view: View): Unit = |
61557 | 225 |
Standard_Thread.fork("hyperlink_url") { |
62248 | 226 |
try { Isabelle_System.open(Url.escape(name)) } |
56461 | 227 |
catch { |
228 |
case exn: Throwable => |
|
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
229 |
GUI_Thread.later { |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
230 |
GUI.error_dialog(view, "System error", GUI.scrollable_text(Exn.message(exn))) |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
231 |
} |
56729 | 232 |
} |
233 |
} |
|
56461 | 234 |
override def toString: String = "URL " + quote(name) |
52980 | 235 |
} |
55876 | 236 |
|
60893 | 237 |
def hyperlink_buffer(focus: Boolean, buffer: Buffer, offset: Text.Offset): Hyperlink = |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
238 |
new Hyperlink { |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
239 |
val external = false |
60893 | 240 |
def follow(view: View): Unit = goto_buffer(focus, view, buffer, offset) |
58545
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
241 |
override def toString: String = "buffer " + quote(JEdit_Lib.buffer_name(buffer)) |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
242 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
243 |
|
60893 | 244 |
def hyperlink_file(focus: Boolean, name: String, line: Int = 0, column: Int = 0): Hyperlink = |
56461 | 245 |
new Hyperlink { |
56494
1b74abf064e1
avoid confusion about pointless cursor movement with external links;
wenzelm
parents:
56462
diff
changeset
|
246 |
val external = false |
60893 | 247 |
def follow(view: View): Unit = goto_file(focus, view, name, line, column) |
56461 | 248 |
override def toString: String = "file " + quote(name) |
249 |
} |
|
55876 | 250 |
|
60893 | 251 |
def hyperlink_source_file(focus: Boolean, source_name: String, line: Int, offset: Symbol.Offset) |
55878 | 252 |
: Option[Hyperlink] = |
253 |
{ |
|
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
254 |
val opt_name = |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
255 |
if (Path.is_wellformed(source_name)) { |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
256 |
if (Path.is_valid(source_name)) { |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
257 |
val path = Path.explode(source_name) |
60988 | 258 |
Some(File.platform_path(Isabelle_System.source_file(path) getOrElse path)) |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
259 |
} |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
260 |
else None |
55878 | 261 |
} |
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
262 |
else Some(source_name) |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
263 |
|
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
264 |
opt_name match { |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
265 |
case Some(name) => |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
266 |
JEdit_Lib.jedit_buffer(name) match { |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
267 |
case Some(buffer) if offset > 0 => |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
268 |
val (line, column) = |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
269 |
JEdit_Lib.buffer_lock(buffer) { |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
270 |
((1, 1) /: |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
271 |
(Symbol.iterator(JEdit_Lib.buffer_text(buffer)). |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
272 |
zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))( |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
273 |
Symbol.advance_line_column) |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
274 |
} |
60893 | 275 |
Some(hyperlink_file(focus, name, line, column)) |
276 |
case _ => Some(hyperlink_file(focus, name, line)) |
|
56458
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
277 |
} |
a8d960baa5c2
simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
wenzelm
parents:
56457
diff
changeset
|
278 |
case None => None |
55878 | 279 |
} |
280 |
} |
|
55876 | 281 |
|
56461 | 282 |
override def hyperlink_command( |
60893 | 283 |
focus: Boolean, snapshot: Document.Snapshot, command: Command, offset: Symbol.Offset = 0) |
284 |
: Option[Hyperlink] = |
|
56461 | 285 |
{ |
286 |
if (snapshot.is_outdated) None |
|
287 |
else { |
|
288 |
snapshot.state.find_command(snapshot.version, command.id) match { |
|
289 |
case None => None |
|
290 |
case Some((node, _)) => |
|
291 |
val file_name = command.node_name.node |
|
292 |
val sources_iterator = |
|
293 |
node.commands.iterator.takeWhile(_ != command).map(_.source) ++ |
|
294 |
(if (offset == 0) Iterator.empty |
|
56462
b64b0cb845fe
more explicit Command.Chunk types, less ooddities;
wenzelm
parents:
56461
diff
changeset
|
295 |
else Iterator.single(command.source(Text.Range(0, command.chunk.decode(offset))))) |
56461 | 296 |
val (line, column) = ((1, 1) /: sources_iterator)(Symbol.advance_line_column) |
60893 | 297 |
Some(hyperlink_file(focus, file_name, line, column)) |
56461 | 298 |
} |
55876 | 299 |
} |
56461 | 300 |
} |
301 |
||
302 |
def hyperlink_command_id( |
|
60893 | 303 |
focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
304 |
: Option[Hyperlink] = |
|
56461 | 305 |
{ |
306 |
snapshot.state.find_command(snapshot.version, id) match { |
|
60893 | 307 |
case Some((node, command)) => hyperlink_command(focus, snapshot, command, offset) |
56461 | 308 |
case None => None |
309 |
} |
|
310 |
} |
|
60874 | 311 |
|
61011 | 312 |
def is_hyperlink_position(snapshot: Document.Snapshot, |
313 |
text_offset: Text.Offset, pos: Position.T): Boolean = |
|
314 |
{ |
|
315 |
pos match { |
|
316 |
case Position.Id_Offset0(id, offset) if offset > 0 => |
|
317 |
snapshot.state.find_command(snapshot.version, id) match { |
|
318 |
case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => |
|
319 |
node.command_start(command) match { |
|
320 |
case Some(start) => text_offset == start + command.chunk.decode(offset) |
|
321 |
case None => false |
|
322 |
} |
|
323 |
case _ => false |
|
324 |
} |
|
325 |
case _ => false |
|
326 |
} |
|
327 |
} |
|
328 |
||
60893 | 329 |
def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) |
330 |
: Option[Hyperlink] = |
|
60874 | 331 |
pos match { |
332 |
case Position.Line_File(line, name) => |
|
333 |
val offset = Position.Offset.unapply(pos) getOrElse 0 |
|
60893 | 334 |
hyperlink_source_file(focus, name, line, offset) |
60874 | 335 |
case Position.Id_Offset0(id, offset) => |
60893 | 336 |
hyperlink_command_id(focus, snapshot, id, offset) |
60874 | 337 |
case _ => None |
338 |
} |
|
339 |
||
60893 | 340 |
def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) |
341 |
: Option[Hyperlink] = |
|
60874 | 342 |
pos match { |
343 |
case Position.Def_Line_File(line, name) => |
|
344 |
val offset = Position.Def_Offset.unapply(pos) getOrElse 0 |
|
60893 | 345 |
hyperlink_source_file(focus, name, line, offset) |
60874 | 346 |
case Position.Def_Id_Offset0(id, offset) => |
60893 | 347 |
hyperlink_command_id(focus, snapshot, id, offset) |
60874 | 348 |
case _ => None |
349 |
} |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
350 |
} |