author | wenzelm |
Mon, 03 Apr 2017 16:50:44 +0200 | |
changeset 65360 | 3ff88fece1f6 |
parent 65359 | 9ca34f0407a9 |
child 65463 | 104502de757c |
permissions | -rw-r--r-- |
43282
5d294220ca43
moved sources -- eliminated Netbeans artifact of jedit package directory;
wenzelm
parents:
41537
diff
changeset
|
1 |
/* Title: Tools/jEdit/src/plugin.scala |
36760 | 2 |
Author: Makarius |
3 |
||
50362 | 4 |
Main plumbing for PIDE infrastructure as jEdit plugin. |
36760 | 5 |
*/ |
34407 | 6 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.jedit |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
8 |
|
34429 | 9 |
|
36015 | 10 |
import isabelle._ |
11 |
||
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
12 |
import javax.swing.JOptionPane |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
|
64858 | 14 |
import java.io.{File => JFile} |
15 |
||
60205
9ee125c3bff7
avoid auto-load dialog while exit/closeAllBuffers is active: the perspective manager happens to indicate this precisely in jEdit 5.2.0;
wenzelm
parents:
60075
diff
changeset
|
16 |
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug, PerspectiveManager} |
65248 | 17 |
import org.gjt.sp.jedit.textarea.JEditTextArea |
50362 | 18 |
import org.gjt.sp.jedit.syntax.ModeProvider |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
19 |
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} |
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
20 |
import org.gjt.sp.util.SyntaxUtilities |
62228
6dfe5b12c5b2
report error on internal channel as well: startup_failure dialog may be too late;
wenzelm
parents:
62227
diff
changeset
|
21 |
import org.gjt.sp.util.Log |
39241 | 22 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
23 |
|
50205 | 24 |
object PIDE |
34618 | 25 |
{ |
65248 | 26 |
/* semantic document content */ |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
27 |
|
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
28 |
def snapshot(view: View): Document.Snapshot = GUI_Thread.now |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
29 |
{ |
64813 | 30 |
Document_Model.get(view.getBuffer) match { |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
31 |
case Some(model) => model.snapshot |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
32 |
case None => error("No document model for current buffer") |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
33 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
34 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
35 |
|
64621 | 36 |
def rendering(view: View): JEdit_Rendering = GUI_Thread.now |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
37 |
{ |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
38 |
val text_area = view.getTextArea |
64882 | 39 |
Document_View.get(text_area) match { |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
40 |
case Some(doc_view) => doc_view.get_rendering() |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
41 |
case None => error("No document view for current text area") |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
42 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
43 |
} |
65277 | 44 |
|
45 |
||
46 |
/* plugin instance */ |
|
47 |
||
48 |
@volatile var _plugin: Plugin = null |
|
49 |
||
50 |
def plugin: Plugin = |
|
51 |
if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin") |
|
52 |
else _plugin |
|
53 |
||
54 |
def options: JEdit_Options = plugin.options |
|
55 |
def resources: JEdit_Resources = plugin.resources |
|
56 |
def session: Session = plugin.session |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
57 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
58 |
|
34618 | 59 |
class Plugin extends EBPlugin |
60 |
{ |
|
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
61 |
/* options */ |
65238 | 62 |
|
65257
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
63 |
private var _options: JEdit_Options = null |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
64 |
private def init_options(): Unit = _options = new JEdit_Options(Options.init()) |
65257
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
65 |
def options: JEdit_Options = _options |
65239
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65238
diff
changeset
|
66 |
|
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
67 |
|
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
68 |
/* resources */ |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
69 |
|
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
70 |
private var _resources: JEdit_Resources = null |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
71 |
private def init_resources() |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
72 |
{ |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
73 |
val options = this.options.value |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
74 |
val session_name = JEdit_Sessions.session_name(options) |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
75 |
val session_base = |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
76 |
try { Sessions.session_base(options, session_name, JEdit_Sessions.session_dirs()) } |
65360 | 77 |
catch { case ERROR(_) => Sessions.Base.pure(options) } |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
78 |
|
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
79 |
_resources = |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
80 |
new JEdit_Resources(session_base.copy(known_theories = |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
81 |
for ((a, b) <- session_base.known_theories) yield (a, b.map(File.platform_path(_))))) |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
82 |
} |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
83 |
def resources: JEdit_Resources = _resources |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
84 |
|
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
85 |
|
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
86 |
/* session */ |
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
87 |
|
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
88 |
private var _session: Session = null |
65264
7e6ecd04b5fe
dynamic session_options for tuning parameters and initial prover options;
wenzelm
parents:
65263
diff
changeset
|
89 |
private def init_session(): Unit = _session = new Session(options.value, resources) |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
90 |
def session: Session = _session |
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
91 |
|
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
92 |
|
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
93 |
/* misc support */ |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
94 |
|
65239
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65238
diff
changeset
|
95 |
val completion_history = new Completion.History_Variable |
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65238
diff
changeset
|
96 |
val spell_checker = new Spell_Checker_Variable |
509a9b0ad02e
avoid global variables with implicit initialization;
wenzelm
parents:
65238
diff
changeset
|
97 |
|
65238 | 98 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
99 |
/* global changes */ |
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
100 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
101 |
def options_changed() |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
102 |
{ |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
103 |
session.global_options.post(Session.Global_Options(options.value)) |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
104 |
delay_load.invoke() |
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
105 |
} |
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
106 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
107 |
def deps_changed() |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
108 |
{ |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
109 |
delay_load.invoke() |
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
110 |
} |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
111 |
|
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
112 |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
113 |
/* theory files */ |
44574 | 114 |
|
62068 | 115 |
lazy val delay_init = |
65249 | 116 |
GUI_Thread.delay_last(options.seconds("editor_load_delay")) |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50209
diff
changeset
|
117 |
{ |
65244 | 118 |
init_models() |
50344
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50209
diff
changeset
|
119 |
} |
608265769ce0
emit bulk edits on initialization of multiple buffers, which greatly improves performance when starting big sessions (e.g. JinjaThreads);
wenzelm
parents:
50209
diff
changeset
|
120 |
|
57582 | 121 |
private val delay_load_active = Synchronized(false) |
122 |
private def delay_load_activated(): Boolean = |
|
123 |
delay_load_active.guarded_access(a => Some((!a, true))) |
|
62068 | 124 |
private def delay_load_action() |
125 |
{ |
|
126 |
if (Isabelle.continuous_checking && delay_load_activated() && |
|
127 |
PerspectiveManager.isPerspectiveEnabled) |
|
44574 | 128 |
{ |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
129 |
if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke() |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
130 |
else { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
131 |
val required_files = |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
132 |
{ |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
133 |
val models = Document_Model.get_models() |
44574 | 134 |
|
62068 | 135 |
val thys = |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
136 |
(for ((node_name, model) <- models.iterator if model.is_theory) |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
137 |
yield (node_name, Position.none)).toList |
65359 | 138 |
val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name) |
46761 | 139 |
|
64839 | 140 |
val aux_files = |
65249 | 141 |
if (options.bool("jedit_auto_resolve")) { |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
142 |
val stable_tip_version = |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
143 |
if (models.forall(p => p._2.is_stable)) |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
144 |
session.current_state().stable_tip_version |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
145 |
else None |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
146 |
stable_tip_version match { |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
147 |
case Some(version) => resources.undefined_blobs(version.nodes) |
64478
812c22e556b9
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
wenzelm
parents:
63754
diff
changeset
|
148 |
case None => delay_load.invoke(); Nil |
57582 | 149 |
} |
62068 | 150 |
} |
151 |
else Nil |
|
152 |
||
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
153 |
(thy_files ::: aux_files).filterNot(models.isDefinedAt(_)) |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
154 |
} |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
155 |
if (required_files.nonEmpty) { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
156 |
try { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
157 |
Standard_Thread.fork("resolve_dependencies") { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
158 |
val loaded_files = |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
159 |
for { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
160 |
name <- required_files |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
161 |
text <- resources.read_file_content(name) |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
162 |
} yield (name, text) |
62068 | 163 |
|
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
164 |
GUI_Thread.later { |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
165 |
try { |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
166 |
Document_Model.provide_files(session, loaded_files) |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
167 |
delay_init.invoke() |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
168 |
} |
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
169 |
finally { delay_load_active.change(_ => false) } |
53715 | 170 |
} |
53074 | 171 |
} |
46761 | 172 |
} |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
173 |
catch { case _: Throwable => delay_load_active.change(_ => false) } |
46761 | 174 |
} |
64835
fd1efd6dd385
resolve dependencies implicitly via File_Model, without jEdit Buffer_Model;
wenzelm
parents:
64818
diff
changeset
|
175 |
else delay_load_active.change(_ => false) |
44606 | 176 |
} |
44574 | 177 |
} |
62068 | 178 |
} |
179 |
||
64478
812c22e556b9
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
wenzelm
parents:
63754
diff
changeset
|
180 |
private lazy val delay_load = |
65249 | 181 |
GUI_Thread.delay_last(options.seconds("editor_load_delay")) { delay_load_action() } |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
182 |
|
64858 | 183 |
private def file_watcher_action(changed: Set[JFile]): Unit = |
65246 | 184 |
if (Document_Model.sync_files(changed)) JEdit_Editor.invoke_generated() |
64858 | 185 |
|
186 |
lazy val file_watcher: File_Watcher = |
|
65249 | 187 |
File_Watcher(file_watcher_action _, options.seconds("editor_load_delay")) |
64858 | 188 |
|
44574 | 189 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
190 |
/* session phase */ |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
191 |
|
65226 | 192 |
val session_phase_changed: Session.Phase => Unit = |
193 |
{ |
|
65317 | 194 |
case Session.Terminated(result) if !result.ok => |
65226 | 195 |
GUI_Thread.later { |
65267 | 196 |
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error", |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
197 |
"Isabelle Syslog", GUI.scrollable_text(session.syslog_content())) |
65226 | 198 |
} |
39735
969ede84aac0
more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;
wenzelm
parents:
39702
diff
changeset
|
199 |
|
65226 | 200 |
case Session.Ready => |
65244 | 201 |
init_models() |
57640
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
202 |
|
65226 | 203 |
if (!Isabelle.continuous_checking) { |
204 |
GUI_Thread.later { |
|
205 |
val answer = |
|
206 |
GUI.confirm_dialog(jEdit.getActiveView, |
|
207 |
"Continuous checking of PIDE document", |
|
208 |
JOptionPane.YES_NO_OPTION, |
|
209 |
"Continuous checking is presently disabled:", |
|
210 |
"editor buffers will remain inactive!", |
|
211 |
"Enable continuous checking now?") |
|
212 |
if (answer == 0) Isabelle.continuous_checking = true |
|
57640
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
213 |
} |
65226 | 214 |
} |
57640
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
215 |
|
65226 | 216 |
delay_load.invoke() |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
217 |
|
65226 | 218 |
case Session.Shutdown => |
219 |
GUI_Thread.later { |
|
220 |
delay_load.revoke() |
|
221 |
delay_init.revoke() |
|
65246 | 222 |
JEdit_Editor.flush() |
65244 | 223 |
exit_models(JEdit_Lib.jedit_buffers().toList) |
65226 | 224 |
} |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
225 |
|
65226 | 226 |
case _ => |
227 |
} |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
228 |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
229 |
|
65244 | 230 |
/* document model and view */ |
231 |
||
232 |
def exit_models(buffers: List[Buffer]) |
|
233 |
{ |
|
234 |
GUI_Thread.now { |
|
235 |
buffers.foreach(buffer => |
|
236 |
JEdit_Lib.buffer_lock(buffer) { |
|
237 |
JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) |
|
238 |
Document_Model.exit(buffer) |
|
239 |
}) |
|
240 |
} |
|
241 |
} |
|
242 |
||
243 |
def init_models() |
|
244 |
{ |
|
245 |
GUI_Thread.now { |
|
65246 | 246 |
JEdit_Editor.flush() |
65244 | 247 |
|
248 |
for { |
|
249 |
buffer <- JEdit_Lib.jedit_buffers() |
|
250 |
if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED) |
|
251 |
} { |
|
252 |
if (buffer.isLoaded) { |
|
253 |
JEdit_Lib.buffer_lock(buffer) { |
|
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
254 |
val node_name = resources.node_name(buffer) |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
255 |
val model = Document_Model.init(session, node_name, buffer) |
65244 | 256 |
for { |
257 |
text_area <- JEdit_Lib.jedit_text_areas(buffer) |
|
258 |
if Document_View.get(text_area).map(_.model) != Some(model) |
|
259 |
} Document_View.init(model, text_area) |
|
260 |
} |
|
261 |
} |
|
262 |
else delay_init.invoke() |
|
263 |
} |
|
264 |
||
65246 | 265 |
JEdit_Editor.invoke_generated() |
65244 | 266 |
} |
267 |
} |
|
268 |
||
269 |
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = |
|
270 |
GUI_Thread.now { |
|
271 |
JEdit_Lib.buffer_lock(buffer) { |
|
272 |
Document_Model.get(buffer) match { |
|
273 |
case Some(model) => Document_View.init(model, text_area) |
|
274 |
case None => |
|
275 |
} |
|
276 |
} |
|
277 |
} |
|
278 |
||
279 |
def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit = |
|
280 |
GUI_Thread.now { |
|
281 |
JEdit_Lib.buffer_lock(buffer) { |
|
282 |
Document_View.exit(text_area) |
|
283 |
} |
|
284 |
} |
|
285 |
||
286 |
||
34618 | 287 |
/* main plugin plumbing */ |
34433 | 288 |
|
65241 | 289 |
@volatile private var startup_failure: Option[Throwable] = None |
290 |
@volatile private var startup_notified = false |
|
291 |
||
34767 | 292 |
override def handleMessage(message: EBMessage) |
34618 | 293 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
294 |
GUI_Thread.assert {} |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
295 |
|
65241 | 296 |
if (startup_failure.isDefined && !startup_notified) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
297 |
message match { |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
298 |
case msg: EditorStarted => |
51616 | 299 |
GUI.error_dialog(null, "Isabelle plugin startup failure", |
65241 | 300 |
GUI.scrollable_text(Exn.message(startup_failure.get)), |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
301 |
"Prover IDE inactive!") |
65241 | 302 |
startup_notified = true |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
303 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
304 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
305 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
306 |
|
65241 | 307 |
if (startup_failure.isEmpty) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
308 |
message match { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
309 |
case msg: EditorStarted => |
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
310 |
if (Distribution.is_identified && !Distribution.is_official) { |
57680 | 311 |
GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing", |
60206 | 312 |
"This is " + Distribution.version + ".", |
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
313 |
"It is for testing only, not for production use.") |
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
314 |
} |
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
315 |
|
64602 | 316 |
val view = jEdit.getActiveView() |
317 |
||
65256 | 318 |
Session_Build.check_dialog(view) |
63747 | 319 |
|
64602 | 320 |
Keymap_Merge.check_dialog(view) |
321 |
||
65246 | 322 |
JEdit_Editor.hyperlink_position(true, Document.Snapshot.init, |
65256 | 323 |
JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view)) |
61277 | 324 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
325 |
case msg: BufferUpdate |
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
326 |
if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING => |
64838 | 327 |
if (msg.getBuffer != null) { |
65244 | 328 |
exit_models(List(msg.getBuffer)) |
65246 | 329 |
JEdit_Editor.invoke_generated() |
64838 | 330 |
} |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
331 |
|
64818
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
332 |
case msg: BufferUpdate |
67a0a563d2b3
clarified buffer events: exit model while loading;
wenzelm
parents:
64817
diff
changeset
|
333 |
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED => |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
334 |
if (session.is_ready) { |
55791
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
335 |
delay_init.invoke() |
5821b1937fa5
clarified init_models: simultaneous initialization of all document models, before flushing edits by regular means (via PIDE.editor.invoke) -- important for consolidated doc_blobs when determining initial edits;
wenzelm
parents:
55784
diff
changeset
|
336 |
delay_load.invoke() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
337 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
338 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
339 |
case msg: EditPaneUpdate |
60215 | 340 |
if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
341 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
342 |
msg.getWhat == EditPaneUpdate.CREATED || |
60215 | 343 |
msg.getWhat == EditPaneUpdate.DESTROYED => |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
344 |
val edit_pane = msg.getEditPane |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
345 |
val buffer = edit_pane.getBuffer |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
346 |
val text_area = edit_pane.getTextArea |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
347 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
348 |
if (buffer != null && text_area != null) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
349 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
350 |
msg.getWhat == EditPaneUpdate.CREATED) { |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
351 |
if (session.is_ready) |
65244 | 352 |
init_view(buffer, text_area) |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
353 |
} |
52867
8d8cb75ab20a
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
wenzelm
parents:
52816
diff
changeset
|
354 |
else { |
65240 | 355 |
Isabelle.dismissed_popups(text_area.getView) |
65244 | 356 |
exit_view(buffer, text_area) |
52867
8d8cb75ab20a
more central Pretty_Tooltip.dismissed_all -- avoid spurious crash of Rich_Text_Area.robust_body in asynchronous mouse_motion_listener;
wenzelm
parents:
52816
diff
changeset
|
357 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
358 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
359 |
if (msg.getWhat == EditPaneUpdate.CREATED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
360 |
Completion_Popup.Text_Area.init(text_area) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
361 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
362 |
if (msg.getWhat == EditPaneUpdate.DESTROYED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
363 |
Completion_Popup.Text_Area.exit(text_area) |
43510
17d431c92575
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
wenzelm
parents:
43487
diff
changeset
|
364 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
365 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
366 |
case msg: PropertiesChanged => |
62264
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
367 |
for { |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
368 |
view <- JEdit_Lib.jedit_views |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
369 |
edit_pane <- JEdit_Lib.jedit_edit_panes(view) |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
370 |
} { |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
371 |
val buffer = edit_pane.getBuffer |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
372 |
val text_area = edit_pane.getTextArea |
65244 | 373 |
if (buffer != null && text_area != null) init_view(buffer, text_area) |
62264
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
374 |
} |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
375 |
|
65249 | 376 |
spell_checker.update(options.value) |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
377 |
session.update_options(options.value) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
378 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
379 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
380 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
381 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
382 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
383 |
|
65260 | 384 |
|
385 |
/* mode provider */ |
|
386 |
||
387 |
private var orig_mode_provider: ModeProvider = null |
|
388 |
private var pide_mode_provider: ModeProvider = null |
|
389 |
||
390 |
def init_mode_provider() |
|
391 |
{ |
|
392 |
orig_mode_provider = ModeProvider.instance |
|
393 |
if (orig_mode_provider.isInstanceOf[ModeProvider]) { |
|
394 |
pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider) |
|
395 |
ModeProvider.instance = pide_mode_provider |
|
396 |
} |
|
397 |
} |
|
398 |
||
399 |
def exit_mode_provider() |
|
400 |
{ |
|
401 |
if (ModeProvider.instance == pide_mode_provider) |
|
402 |
ModeProvider.instance = orig_mode_provider |
|
403 |
} |
|
404 |
||
405 |
||
406 |
/* start and stop */ |
|
407 |
||
34618 | 408 |
override def start() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
409 |
{ |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
410 |
Debug.DISABLE_SEARCH_DIALOG_POOL = true |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
411 |
|
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
412 |
|
65257
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
413 |
/* strict initialization */ |
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
414 |
|
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
415 |
init_options() |
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
416 |
init_resources() |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
417 |
init_session() |
65262
0fe4ebab9fdf
resources are part of early/strict initialization, but session_base is permissive to avoid crash of "isabelle jedit -l BAD";
wenzelm
parents:
65261
diff
changeset
|
418 |
PIDE._plugin = this |
65257
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
419 |
|
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
420 |
|
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
421 |
/* non-strict initialization */ |
2307b91159bb
more explicit strict vs. non-strict initialization;
wenzelm
parents:
65256
diff
changeset
|
422 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
423 |
try { |
65242 | 424 |
completion_history.load() |
65249 | 425 |
spell_checker.update(options.value) |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
426 |
|
65261 | 427 |
SyntaxUtilities.setStyleExtender(Syntax_Style.Extender) |
65260 | 428 |
init_mode_provider() |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
429 |
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
430 |
|
65241 | 431 |
startup_failure = None |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
432 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
433 |
catch { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
434 |
case exn: Throwable => |
65241 | 435 |
startup_failure = Some(exn) |
436 |
startup_notified = false |
|
62228
6dfe5b12c5b2
report error on internal channel as well: startup_failure dialog may be too late;
wenzelm
parents:
62227
diff
changeset
|
437 |
Log.log(Log.ERROR, this, exn) |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
438 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
439 |
} |
34618 | 440 |
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
441 |
override def stop() |
34618 | 442 |
{ |
65261 | 443 |
exit_mode_provider() |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
444 |
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
445 |
|
65241 | 446 |
if (startup_failure.isEmpty) { |
65249 | 447 |
options.value.save_prefs() |
65242 | 448 |
completion_history.value.save() |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
449 |
} |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
450 |
|
65244 | 451 |
exit_models(JEdit_Lib.jedit_buffers().toList) |
65263
c97abf0fa0c1
strict initialization of plugin.session: no user errors to be expected before session.start;
wenzelm
parents:
65262
diff
changeset
|
452 |
session.stop() |
65245 | 453 |
file_watcher.shutdown() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
454 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
455 |
} |