author | wenzelm |
Mon, 06 Apr 2020 12:53:45 +0200 | |
changeset 71704 | b9a5eb0f3b43 |
parent 71692 | f8e52c0152fe |
child 72823 | ab1a49ac456b |
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 |
70016 | 17 |
import org.gjt.sp.jedit.io.{VFSManager, VFSFile} |
52971
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 |
|
66083 | 20 |
class JEdit_Editor extends Editor[View] |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
21 |
{ |
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
22 |
/* session */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
23 |
|
52980 | 24 |
override def session: Session = PIDE.session |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
25 |
|
66084 | 26 |
def flush_edits(hidden: Boolean = false, purge: Boolean = false): Unit = |
64817 | 27 |
GUI_Thread.require { |
64867 | 28 |
val (doc_blobs, edits) = Document_Model.flush_edits(hidden, purge) |
64817 | 29 |
session.update(doc_blobs, edits) |
30 |
} |
|
66084 | 31 |
override def flush(): Unit = flush_edits() |
32 |
def purge() { flush_edits(purge = true) } |
|
64867 | 33 |
|
64524
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64521
diff
changeset
|
34 |
private val delay1_flush = |
71704 | 35 |
Delay.last(PIDE.options.seconds("editor_input_delay"), gui = true) { flush() } |
54461 | 36 |
|
64524
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64521
diff
changeset
|
37 |
private val delay2_flush = |
71704 | 38 |
Delay.first(PIDE.options.seconds("editor_generated_input_delay"), gui = true) { flush() } |
64521
1aef5a0e18d7
delay_first for machine generated editor events: avoid starvation, e.g. when operating on big sessions;
wenzelm
parents:
62248
diff
changeset
|
39 |
|
64524
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64521
diff
changeset
|
40 |
def invoke(): Unit = delay1_flush.invoke() |
e6a3c55b929b
explicit option editor_generated_input_delay, which is more aggressive by default;
wenzelm
parents:
64521
diff
changeset
|
41 |
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() } |
54461 | 42 |
|
66458
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
43 |
def shutdown(): Unit = |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
44 |
GUI_Thread.require { |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
45 |
delay1_flush.revoke() |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
46 |
delay2_flush.revoke() |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
47 |
Document_Model.flush_edits(hidden = false, purge = false) |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
48 |
} |
42d0d5c77c78
more robust shutdown, e.g. when plugin is stopped;
wenzelm
parents:
66101
diff
changeset
|
49 |
|
64799 | 50 |
def visible_node(name: Document.Node.Name): Boolean = |
64840 | 51 |
(for { |
52 |
text_area <- JEdit_Lib.jedit_text_areas() |
|
64882 | 53 |
doc_view <- Document_View.get(text_area) |
64840 | 54 |
} yield doc_view.model.node_name).contains(name) |
64799 | 55 |
|
52977
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
56 |
|
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
57 |
/* current situation */ |
15254e32d299
central management of Document.Overlays, independent of Document_Model;
wenzelm
parents:
52974
diff
changeset
|
58 |
|
52980 | 59 |
override def current_node(view: View): Option[Document.Node.Name] = |
64813 | 60 |
GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.node_name) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
61 |
|
52980 | 62 |
override def current_node_snapshot(view: View): Option[Document.Snapshot] = |
64813 | 63 |
GUI_Thread.require { Document_Model.get(view.getBuffer).map(_.snapshot()) } |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
64 |
|
52980 | 65 |
override def node_snapshot(name: Document.Node.Name): Document.Snapshot = |
52974 | 66 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
67 |
GUI_Thread.require {} |
64817 | 68 |
Document_Model.get(name) match { |
69 |
case Some(model) => model.snapshot |
|
52974 | 70 |
case None => session.snapshot(name) |
71 |
} |
|
72 |
} |
|
73 |
||
53844
71f103629327
skip ignored commands, similar to former proper_command_at (see d68ea01d5084) -- relevant to Output, Query_Operation etc.;
wenzelm
parents:
52980
diff
changeset
|
74 |
override def current_command(view: View, snapshot: Document.Snapshot): Option[Command] = |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
75 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
76 |
GUI_Thread.require {} |
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
77 |
|
54325
2c4155003352
clarified Editor.current_command: allow outdated snapshot;
wenzelm
parents:
53845
diff
changeset
|
78 |
val text_area = view.getTextArea |
54528 | 79 |
val buffer = view.getBuffer |
80 |
||
64882 | 81 |
Document_View.get(text_area) match { |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54706
diff
changeset
|
82 |
case Some(doc_view) if doc_view.model.is_theory => |
65199
6bd7081f8319
clarified current_command: index refers to node content, negative index means first command;
wenzelm
parents:
65196
diff
changeset
|
83 |
snapshot.current_command(doc_view.model.node_name, text_area.getCaretPosition) |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54706
diff
changeset
|
84 |
case _ => |
64813 | 85 |
Document_Model.get(buffer) match { |
54531
8330faaeebd5
restrict node_required status and Theories panel to actual theories;
wenzelm
parents:
54528
diff
changeset
|
86 |
case Some(model) if !model.is_theory => |
65187 | 87 |
snapshot.version.nodes.commands_loading(model.node_name).headOption |
54528 | 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 |
|
66101
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
94 |
/* overlays */ |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
95 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
96 |
override def node_overlays(name: Document.Node.Name): Document.Node.Overlays = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
97 |
Document_Model.node_overlays(name) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
98 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
99 |
override def insert_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
100 |
Document_Model.insert_overlay(command, fn, args) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
101 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
102 |
override def remove_overlay(command: Command, fn: String, args: List[String]): Unit = |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
103 |
Document_Model.remove_overlay(command, fn, args) |
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
104 |
|
0f0f294e314f
maintain overlays within main state of document models;
wenzelm
parents:
66094
diff
changeset
|
105 |
|
55877 | 106 |
/* navigation */ |
52980 | 107 |
|
56413 | 108 |
def push_position(view: View) |
109 |
{ |
|
110 |
val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin") |
|
111 |
if (navigator != null) { |
|
59080
611914621edb
added Untyped.method convenience (for *this* class only);
wenzelm
parents:
58545
diff
changeset
|
112 |
try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) } |
56413 | 113 |
catch { case _: NoSuchMethodException => } |
114 |
} |
|
115 |
} |
|
116 |
||
60893 | 117 |
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
|
118 |
{ |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
119 |
GUI_Thread.require {} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
120 |
|
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
121 |
push_position(view) |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
122 |
|
60893 | 123 |
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
|
124 |
try { view.getTextArea.moveCaretPosition(offset) } |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
125 |
catch { |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
126 |
case _: ArrayIndexOutOfBoundsException => |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
127 |
case _: IllegalArgumentException => |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
128 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
129 |
} |
30b75b7958d6
citation tooltip/hyperlink based on open buffers with .bib files;
wenzelm
parents:
57878
diff
changeset
|
130 |
|
64653 | 131 |
def goto_file(focus: Boolean, view: View, name: String): Unit = |
66605
261dcd52c5a0
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
wenzelm
parents:
66458
diff
changeset
|
132 |
goto_file(focus, view, Line.Node_Position.offside(name)) |
64653 | 133 |
|
134 |
def goto_file(focus: Boolean, view: View, pos: Line.Node_Position) |
|
52980 | 135 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
136 |
GUI_Thread.require {} |
52980 | 137 |
|
56413 | 138 |
push_position(view) |
139 |
||
64653 | 140 |
val name = pos.name |
141 |
val line = pos.line |
|
142 |
val column = pos.column |
|
143 |
||
54706 | 144 |
JEdit_Lib.jedit_buffer(name) match { |
52980 | 145 |
case Some(buffer) => |
60893 | 146 |
if (focus) view.goToBuffer(buffer) else view.showBuffer(buffer) |
52980 | 147 |
val text_area = view.getTextArea |
148 |
||
149 |
try { |
|
64653 | 150 |
val line_start = text_area.getBuffer.getLineStartOffset(line) |
52980 | 151 |
text_area.moveCaretPosition(line_start) |
64653 | 152 |
if (column > 0) text_area.moveCaretPosition(line_start + column) |
52980 | 153 |
} |
154 |
catch { |
|
155 |
case _: ArrayIndexOutOfBoundsException => |
|
156 |
case _: IllegalArgumentException => |
|
157 |
} |
|
158 |
||
70016 | 159 |
case None => |
70167
b33f28c81ba9
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
wenzelm
parents:
70016
diff
changeset
|
160 |
val is_dir = |
70016 | 161 |
try { |
162 |
val vfs = VFSManager.getVFSForPath(name) |
|
163 |
val vfs_file = vfs._getFile((), name, view) |
|
70167
b33f28c81ba9
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
wenzelm
parents:
70016
diff
changeset
|
164 |
vfs_file != null && vfs_file.getType == VFSFile.DIRECTORY |
70016 | 165 |
} |
166 |
catch { case ERROR(_) => false } |
|
54706 | 167 |
|
70167
b33f28c81ba9
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
wenzelm
parents:
70016
diff
changeset
|
168 |
if (is_dir) VFSBrowser.browseDirectory(view, name) |
b33f28c81ba9
clarified goto_file (again): treat bad entry as plain file to open empty buffer instead of error (amending a8142ac5e4b6);
wenzelm
parents:
70016
diff
changeset
|
169 |
else { |
70016 | 170 |
val args = |
171 |
if (line <= 0) Array(name) |
|
172 |
else if (column <= 0) Array(name, "+line:" + (line + 1)) |
|
173 |
else Array(name, "+line:" + (line + 1) + "," + (column + 1)) |
|
174 |
jEdit.openFiles(view, null, args) |
|
175 |
} |
|
52980 | 176 |
} |
177 |
} |
|
178 |
||
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
179 |
def goto_doc(view: View, path: Path) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
180 |
{ |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
181 |
if (path.is_file) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
182 |
goto_file(true, view, File.platform_path(path)) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
183 |
else { |
71692 | 184 |
Isabelle_Thread.fork(name = "documentation") { |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
185 |
try { Doc.view(path) } |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
186 |
catch { |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
187 |
case exn: Throwable => |
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
188 |
GUI_Thread.later { |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
189 |
GUI.error_dialog(view, |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
190 |
"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
|
191 |
} |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
192 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
193 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
194 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
195 |
} |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
196 |
|
55877 | 197 |
|
198 |
/* hyperlinks */ |
|
199 |
||
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
200 |
def hyperlink_doc(name: String): Option[Hyperlink] = |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
201 |
Doc.contents().collectFirst({ |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
202 |
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
|
203 |
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
|
204 |
new Hyperlink { |
71601 | 205 |
override val external: Boolean = !path.is_file |
61660
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
206 |
def follow(view: View): Unit = goto_doc(view, path) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
207 |
override def toString: String = "doc " + quote(name) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
208 |
}) |
78b371644654
added antiquotation @{doc}, e.g. useful for demonstration purposes;
wenzelm
parents:
61557
diff
changeset
|
209 |
|
56461 | 210 |
def hyperlink_url(name: String): Hyperlink = |
211 |
new Hyperlink { |
|
64663 | 212 |
override val external = true |
56729 | 213 |
def follow(view: View): Unit = |
71692 | 214 |
Isabelle_Thread.fork(name = "hyperlink_url") { |
69901 | 215 |
try { Isabelle_System.open(Url.escape_name(name)) } |
56461 | 216 |
catch { |
217 |
case exn: Throwable => |
|
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
218 |
GUI_Thread.later { |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
61728
diff
changeset
|
219 |
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
|
220 |
} |
56729 | 221 |
} |
222 |
} |
|
56461 | 223 |
override def toString: String = "URL " + quote(name) |
52980 | 224 |
} |
55876 | 225 |
|
64653 | 226 |
def hyperlink_file(focus: Boolean, name: String): Hyperlink = |
66605
261dcd52c5a0
less aggressive default position: prefer persistent defaults maintained by jEdit (amending 89c5bb2a2128);
wenzelm
parents:
66458
diff
changeset
|
227 |
hyperlink_file(focus, Line.Node_Position.offside(name)) |
64653 | 228 |
|
229 |
def hyperlink_file(focus: Boolean, pos: Line.Node_Position): Hyperlink = |
|
56461 | 230 |
new Hyperlink { |
64653 | 231 |
def follow(view: View): Unit = goto_file(focus, view, pos) |
232 |
override def toString: String = "file " + quote(pos.name) |
|
56461 | 233 |
} |
55876 | 234 |
|
64829
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
235 |
def hyperlink_model(focus: Boolean, model: Document_Model, offset: Text.Offset): Hyperlink = |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
236 |
model match { |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
237 |
case file_model: File_Model => |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
238 |
val pos = |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
239 |
try { file_model.node_position(offset) } |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
240 |
catch { case ERROR(_) => Line.Node_Position(file_model.node_name.node) } |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
241 |
hyperlink_file(focus, pos) |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
242 |
case buffer_model: Buffer_Model => |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
243 |
new Hyperlink { |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
244 |
def follow(view: View): Unit = goto_buffer(focus, view, buffer_model.buffer, offset) |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
245 |
override def toString: String = "buffer " + quote(model.node_name.node) |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
246 |
} |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
247 |
} |
07f209e957bc
refer to bibtex entries via general Document_Model, instead of editor buffers;
wenzelm
parents:
64817
diff
changeset
|
248 |
|
64653 | 249 |
def hyperlink_source_file(focus: Boolean, source_name: String, line1: Int, offset: Symbol.Offset) |
55878 | 250 |
: Option[Hyperlink] = |
251 |
{ |
|
64657 | 252 |
for (name <- PIDE.resources.source_file(source_name)) yield { |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
253 |
def hyperlink(pos: Line.Position) = |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
254 |
hyperlink_file(focus, Line.Node_Position(name, pos)) |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
255 |
|
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
256 |
if (offset > 0) { |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
257 |
PIDE.resources.get_file_content(PIDE.resources.node_name(name)) match { |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
258 |
case Some(text) => |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
259 |
hyperlink( |
64657 | 260 |
(Line.Position.zero /: |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
261 |
(Symbol.iterator(text). |
65196
e8760a98db78
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
wenzelm
parents:
65187
diff
changeset
|
262 |
zipWithIndex.takeWhile(p => p._2 < offset - 1).map(_._1)))(_.advance(_))) |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
263 |
case None => |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
264 |
hyperlink(Line.Position((line1 - 1) max 0)) |
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
265 |
} |
55878 | 266 |
} |
64841
d53696aed874
added node_name(String): imitate jEdit buffer operations;
wenzelm
parents:
64840
diff
changeset
|
267 |
else hyperlink(Line.Position((line1 - 1) max 0)) |
55878 | 268 |
} |
269 |
} |
|
55876 | 270 |
|
56461 | 271 |
override def hyperlink_command( |
64664 | 272 |
focus: Boolean, snapshot: Document.Snapshot, id: Document_ID.Generic, offset: Symbol.Offset = 0) |
60893 | 273 |
: Option[Hyperlink] = |
56461 | 274 |
{ |
275 |
if (snapshot.is_outdated) None |
|
64665 | 276 |
else snapshot.find_command_position(id, offset).map(hyperlink_file(focus, _)) |
56461 | 277 |
} |
278 |
||
61011 | 279 |
def is_hyperlink_position(snapshot: Document.Snapshot, |
280 |
text_offset: Text.Offset, pos: Position.T): Boolean = |
|
281 |
{ |
|
282 |
pos match { |
|
64667 | 283 |
case Position.Item_Id(id, range) if range.start > 0 => |
64665 | 284 |
snapshot.find_command(id) match { |
61011 | 285 |
case Some((node, command)) if snapshot.version.nodes(command.node_name) eq node => |
286 |
node.command_start(command) match { |
|
64667 | 287 |
case Some(start) => text_offset == start + command.chunk.decode(range.start) |
61011 | 288 |
case None => false |
289 |
} |
|
290 |
case _ => false |
|
291 |
} |
|
292 |
case _ => false |
|
293 |
} |
|
294 |
} |
|
295 |
||
60893 | 296 |
def hyperlink_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) |
297 |
: Option[Hyperlink] = |
|
60874 | 298 |
pos match { |
64667 | 299 |
case Position.Item_File(name, line, range) => |
300 |
hyperlink_source_file(focus, name, line, range.start) |
|
301 |
case Position.Item_Id(id, range) => |
|
302 |
hyperlink_command(focus, snapshot, id, range.start) |
|
60874 | 303 |
case _ => None |
304 |
} |
|
305 |
||
60893 | 306 |
def hyperlink_def_position(focus: Boolean, snapshot: Document.Snapshot, pos: Position.T) |
307 |
: Option[Hyperlink] = |
|
60874 | 308 |
pos match { |
64667 | 309 |
case Position.Item_Def_File(name, line, range) => |
310 |
hyperlink_source_file(focus, name, line, range.start) |
|
311 |
case Position.Item_Def_Id(id, range) => |
|
312 |
hyperlink_command(focus, snapshot, id, range.start) |
|
60874 | 313 |
case _ => None |
314 |
} |
|
66094 | 315 |
|
316 |
||
317 |
/* dispatcher thread */ |
|
318 |
||
319 |
override def assert_dispatcher[A](body: => A): A = GUI_Thread.assert(body) |
|
320 |
override def require_dispatcher[A](body: => A): A = GUI_Thread.require(body) |
|
321 |
override def send_dispatcher(body: => Unit): Unit = GUI_Thread.later(body) |
|
322 |
override def send_wait_dispatcher(body: => Unit): Unit = GUI_Thread.now(body) |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
diff
changeset
|
323 |
} |