author | wenzelm |
Thu, 10 Nov 2016 10:20:11 +0100 | |
changeset 64478 | 812c22e556b9 |
parent 63754 | 23b013b6b2fb |
child 64521 | 1aef5a0e18d7 |
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 |
|
49246 | 14 |
import scala.swing.{ListView, ScrollPane} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
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} |
53487 | 17 |
import org.gjt.sp.jedit.gui.AboutDialog |
39043 | 18 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
19 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
50362 | 20 |
import org.gjt.sp.jedit.syntax.ModeProvider |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
21 |
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
|
22 |
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
|
23 |
import org.gjt.sp.util.Log |
39241 | 24 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
25 |
|
50205 | 26 |
object PIDE |
34618 | 27 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
28 |
/* plugin instance */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
29 |
|
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
30 |
val options = new JEdit_Options |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
31 |
val completion_history = new Completion.History_Variable |
56558
05c833d402bc
tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents:
56557
diff
changeset
|
32 |
val spell_checker = new Spell_Checker_Variable |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
33 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
34 |
@volatile var startup_failure: Option[Throwable] = None |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
35 |
@volatile var startup_notified = false |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
36 |
|
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
37 |
@volatile var plugin: Plugin = null |
60835 | 38 |
@volatile var session: Session = new Session(JEdit_Resources.empty) |
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
39 |
|
62068 | 40 |
def options_changed() { if (plugin != null) plugin.options_changed() } |
41 |
def deps_changed() { if (plugin != null) plugin.deps_changed() } |
|
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
52807
diff
changeset
|
42 |
|
56208 | 43 |
def resources(): JEdit_Resources = |
44 |
session.resources.asInstanceOf[JEdit_Resources] |
|
44955 | 45 |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52876
diff
changeset
|
46 |
lazy val editor = new JEdit_Editor |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52876
diff
changeset
|
47 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
48 |
|
53244 | 49 |
/* popups */ |
50 |
||
51 |
def dismissed_popups(view: View): Boolean = |
|
52 |
{ |
|
53272 | 53 |
var dismissed = false |
54 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
55 |
JEdit_Lib.jedit_text_areas(view).foreach(text_area => |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
56 |
if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true) |
53272 | 57 |
|
58 |
if (Pretty_Tooltip.dismissed_all()) dismissed = true |
|
59 |
||
60 |
dismissed |
|
53244 | 61 |
} |
62 |
||
63 |
||
43449 | 64 |
/* document model and view */ |
65 |
||
59077
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
66 |
def document_model(buffer: JEditBuffer): Option[Document_Model] = |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
67 |
buffer match { |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
68 |
case b: Buffer => Document_Model(b) |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
69 |
case _ => None |
7e0d3da6e6d8
node-specific syntax, with base_syntax as default;
wenzelm
parents:
58928
diff
changeset
|
70 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
71 |
|
55712 | 72 |
def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area) |
43449 | 73 |
|
44379 | 74 |
def document_views(buffer: Buffer): List[Document_View] = |
75 |
for { |
|
49406 | 76 |
text_area <- JEdit_Lib.jedit_text_areas(buffer).toList |
54529 | 77 |
doc_view <- document_view(text_area) |
78 |
} yield doc_view |
|
44379 | 79 |
|
54522 | 80 |
def document_models(): List[Document_Model] = |
81 |
for { |
|
82 |
buffer <- JEdit_Lib.jedit_buffers().toList |
|
83 |
model <- document_model(buffer) |
|
84 |
} yield model |
|
85 |
||
86 |
def document_blobs(): Document.Blobs = |
|
55783 | 87 |
Document.Blobs( |
88 |
(for { |
|
89 |
buffer <- JEdit_Lib.jedit_buffers() |
|
90 |
model <- document_model(buffer) |
|
91 |
blob <- model.get_blob() |
|
92 |
} yield (model.node_name -> blob)).toMap) |
|
54522 | 93 |
|
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
|
94 |
def exit_models(buffers: List[Buffer]) |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
95 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
96 |
GUI_Thread.now { |
54461 | 97 |
PIDE.editor.flush() |
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
|
98 |
buffers.foreach(buffer => |
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
|
99 |
JEdit_Lib.buffer_lock(buffer) { |
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
|
100 |
JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit) |
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
|
101 |
Document_Model.exit(buffer) |
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
|
102 |
}) |
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
|
103 |
} |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
104 |
} |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
105 |
|
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
|
106 |
def init_models() |
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
|
107 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
108 |
GUI_Thread.now { |
54461 | 109 |
PIDE.editor.flush() |
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
|
110 |
|
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
|
111 |
for { |
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 |
buffer <- JEdit_Lib.jedit_buffers() |
62068 | 113 |
if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED) |
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
|
114 |
} { |
62068 | 115 |
if (buffer.isLoaded) { |
116 |
JEdit_Lib.buffer_lock(buffer) { |
|
117 |
val node_name = resources.node_name(buffer) |
|
118 |
val model = Document_Model.init(session, buffer, node_name, document_model(buffer)) |
|
119 |
for { |
|
120 |
text_area <- JEdit_Lib.jedit_text_areas(buffer) |
|
121 |
if document_view(text_area).map(_.model) != Some(model) |
|
122 |
} Document_View.init(model, text_area) |
|
123 |
} |
|
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
|
124 |
} |
62068 | 125 |
else if (plugin != null) plugin.delay_init.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
|
126 |
} |
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
|
127 |
|
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
|
128 |
PIDE.editor.invoke() |
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
|
129 |
} |
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
|
130 |
} |
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
|
131 |
|
56774 | 132 |
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
133 |
GUI_Thread.now { |
56774 | 134 |
JEdit_Lib.buffer_lock(buffer) { |
135 |
document_model(buffer) match { |
|
136 |
case Some(model) => Document_View.init(model, text_area) |
|
137 |
case None => |
|
138 |
} |
|
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
|
139 |
} |
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
|
140 |
} |
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
|
141 |
|
56774 | 142 |
def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
143 |
GUI_Thread.now { |
56774 | 144 |
JEdit_Lib.buffer_lock(buffer) { |
145 |
Document_View.exit(text_area) |
|
146 |
} |
|
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
|
147 |
} |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
148 |
|
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
149 |
|
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
150 |
/* current document content */ |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
151 |
|
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
152 |
def snapshot(view: View): Document.Snapshot = GUI_Thread.now |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
153 |
{ |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
154 |
val buffer = view.getBuffer |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
155 |
document_model(buffer) match { |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
156 |
case Some(model) => model.snapshot |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
157 |
case None => error("No document model for current buffer") |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
158 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
159 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
160 |
|
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
161 |
def rendering(view: View): Rendering = GUI_Thread.now |
55621
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
162 |
{ |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
163 |
val text_area = view.getTextArea |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
164 |
document_view(text_area) match { |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
165 |
case Some(doc_view) => doc_view.get_rendering() |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
166 |
case None => error("No document view for current text area") |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
167 |
} |
8d69c15b6fb9
added PIDE.snapshot, PIDE.rendering for convenience;
wenzelm
parents:
55618
diff
changeset
|
168 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
169 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
170 |
|
34429 | 171 |
|
34618 | 172 |
class Plugin extends EBPlugin |
173 |
{ |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
174 |
/* 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
|
175 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
176 |
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
|
177 |
{ |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
178 |
PIDE.session.global_options.post(Session.Global_Options(PIDE.options.value)) |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
179 |
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
|
180 |
} |
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
|
181 |
|
56316
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
182 |
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
|
183 |
{ |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
184 |
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
|
185 |
} |
b1cf8ddc2e04
propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
wenzelm
parents:
56208
diff
changeset
|
186 |
|
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
|
187 |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
188 |
/* theory files */ |
44574 | 189 |
|
62068 | 190 |
lazy val delay_init = |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
191 |
GUI_Thread.delay_last(PIDE.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
|
192 |
{ |
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
|
193 |
PIDE.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
|
194 |
} |
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
|
195 |
|
57582 | 196 |
private val delay_load_active = Synchronized(false) |
197 |
private def delay_load_activated(): Boolean = |
|
198 |
delay_load_active.guarded_access(a => Some((!a, true))) |
|
62068 | 199 |
private def delay_load_action() |
200 |
{ |
|
201 |
if (Isabelle.continuous_checking && delay_load_activated() && |
|
202 |
PerspectiveManager.isPerspectiveEnabled) |
|
44574 | 203 |
{ |
62068 | 204 |
try { |
205 |
val view = jEdit.getActiveView() |
|
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44955
diff
changeset
|
206 |
|
62068 | 207 |
val buffers = JEdit_Lib.jedit_buffers().toList |
208 |
if (buffers.forall(_.isLoaded)) { |
|
209 |
def loaded_buffer(name: String): Boolean = |
|
210 |
buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name) |
|
44574 | 211 |
|
62068 | 212 |
val thys = |
213 |
for { |
|
214 |
buffer <- buffers |
|
215 |
model <- PIDE.document_model(buffer) |
|
216 |
if model.is_theory |
|
217 |
} yield (model.node_name, Position.none) |
|
46761 | 218 |
|
62068 | 219 |
val thy_info = new Thy_Info(PIDE.resources) |
220 |
val thy_files = thy_info.dependencies("", thys).deps.map(_.name.node) |
|
60916
a6e2a667b0a8
resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
wenzelm
parents:
60910
diff
changeset
|
221 |
|
62068 | 222 |
val aux_files = |
223 |
if (PIDE.options.bool("jedit_auto_resolve")) { |
|
224 |
PIDE.editor.stable_tip_version() match { |
|
225 |
case Some(version) => PIDE.resources.undefined_blobs(version.nodes).map(_.node) |
|
64478
812c22e556b9
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
wenzelm
parents:
63754
diff
changeset
|
226 |
case None => delay_load.invoke(); Nil |
57582 | 227 |
} |
62068 | 228 |
} |
229 |
else Nil |
|
230 |
||
231 |
val files = |
|
232 |
(thy_files ::: aux_files).filter(file => |
|
233 |
!loaded_buffer(file) && PIDE.resources.check_file(file)) |
|
44606 | 234 |
|
62068 | 235 |
if (files.nonEmpty) { |
236 |
if (PIDE.options.bool("jedit_auto_load")) { |
|
237 |
files.foreach(file => jEdit.openFile(null: View, file)) |
|
238 |
} |
|
239 |
else { |
|
240 |
val files_list = new ListView(files.sorted) |
|
241 |
for (i <- 0 until files.length) |
|
242 |
files_list.selection.indices += i |
|
243 |
||
244 |
val answer = |
|
245 |
GUI.confirm_dialog(view, |
|
246 |
"Auto loading of required files", |
|
247 |
JOptionPane.YES_NO_OPTION, |
|
248 |
"The following files are required to resolve theory imports.", |
|
249 |
"Reload selected files now?", |
|
250 |
new ScrollPane(files_list), |
|
251 |
new Isabelle.Continuous_Checking) |
|
252 |
if (answer == 0) { |
|
253 |
files.foreach(file => |
|
254 |
if (files_list.selection.items.contains(file)) |
|
255 |
jEdit.openFile(null: View, file)) |
|
53715 | 256 |
} |
53074 | 257 |
} |
46761 | 258 |
} |
259 |
} |
|
62068 | 260 |
else delay_load.invoke() |
44606 | 261 |
} |
62068 | 262 |
finally { delay_load_active.change(_ => false) } |
44574 | 263 |
} |
62068 | 264 |
} |
265 |
||
64478
812c22e556b9
more robust jedit_auto_resolve: avoid losing events deps_changed() / delay_load.invoke();
wenzelm
parents:
63754
diff
changeset
|
266 |
private lazy val delay_load = |
62068 | 267 |
GUI_Thread.delay_last(PIDE.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
|
268 |
|
44574 | 269 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
270 |
/* session phase */ |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
271 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
272 |
private val session_phase = |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
273 |
Session.Consumer[Session.Phase](getClass.getName) { |
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
274 |
case Session.Inactive | Session.Failed => |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
275 |
GUI_Thread.later { |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
276 |
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated", |
56775
59f70b89e5fd
improved syslog performance -- avoid denial-of-service e.g. with threads_trace = 5 and active Syslog dockable;
wenzelm
parents:
56774
diff
changeset
|
277 |
"Isabelle Syslog", GUI.scrollable_text(PIDE.session.syslog_content())) |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
278 |
} |
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
|
279 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
280 |
case Session.Ready => |
60910 | 281 |
Debugger.init_session(PIDE.session) |
60075 | 282 |
PIDE.session.update_options(PIDE.options.value) |
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
283 |
PIDE.init_models() |
57640
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
284 |
|
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
285 |
if (!Isabelle.continuous_checking) { |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
286 |
GUI_Thread.later { |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
287 |
val answer = |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
288 |
GUI.confirm_dialog(jEdit.getActiveView, |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
289 |
"Continuous checking of PIDE document", |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
290 |
JOptionPane.YES_NO_OPTION, |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
291 |
"Continuous checking is presently disabled:", |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
292 |
"editor buffers will remain inactive!", |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
293 |
"Enable continuous checking now?") |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
294 |
if (answer == 0) Isabelle.continuous_checking = true |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
295 |
} |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
296 |
} |
0a28cf866d5d
reconfirm continuous checking on startup, to address common trap of disabling it accidentally;
wenzelm
parents:
57612
diff
changeset
|
297 |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56715
diff
changeset
|
298 |
delay_load.invoke() |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
299 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
300 |
case Session.Shutdown => |
62062
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
301 |
GUI_Thread.later { |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
302 |
delay_load.revoke() |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
303 |
PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) |
ee610059b0e9
fewer use of GUI_Thread.now to reduce danger of deadlock on shutdown;
wenzelm
parents:
62051
diff
changeset
|
304 |
} |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
305 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
306 |
case _ => |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
307 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
308 |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
309 |
|
34618 | 310 |
/* main plugin plumbing */ |
34433 | 311 |
|
34767 | 312 |
override def handleMessage(message: EBMessage) |
34618 | 313 |
{ |
57612
990ffb84489b
clarified module name: facilitate alternative GUI frameworks;
wenzelm
parents:
57611
diff
changeset
|
314 |
GUI_Thread.assert {} |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
315 |
|
50205 | 316 |
if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
317 |
message match { |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
318 |
case msg: EditorStarted => |
51616 | 319 |
GUI.error_dialog(null, "Isabelle plugin startup failure", |
320 |
GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)), |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
321 |
"Prover IDE inactive!") |
50205 | 322 |
PIDE.startup_notified = true |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
323 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
324 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
325 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
326 |
|
50205 | 327 |
if (PIDE.startup_failure.isEmpty) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
328 |
message match { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
329 |
case msg: EditorStarted => |
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
330 |
if (Distribution.is_identified && !Distribution.is_official) { |
57680 | 331 |
GUI.warning_dialog(jEdit.getActiveView, "Isabelle version for testing", |
60206 | 332 |
"This is " + Distribution.version + ".", |
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
333 |
"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
|
334 |
} |
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
57640
diff
changeset
|
335 |
|
63754 | 336 |
Session_Build.session_build(jEdit.getActiveView()) |
63747 | 337 |
|
63754 | 338 |
Keymap_Merge.check_dialog(jEdit.getActiveView()) |
61277 | 339 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
340 |
case msg: BufferUpdate |
57611
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
341 |
if msg.getWhat == BufferUpdate.LOADED || |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
342 |
msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
343 |
msg.getWhat == BufferUpdate.CLOSING => |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
344 |
|
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
345 |
if (msg.getWhat == BufferUpdate.CLOSING) { |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
346 |
val buffer = msg.getBuffer |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
347 |
if (buffer != null) PIDE.editor.remove_node(PIDE.resources.node_name(msg.getBuffer)) |
b6256ea3b7c5
proper change of perspective for removed nodes (stemming from closed buffers);
wenzelm
parents:
57582
diff
changeset
|
348 |
} |
50205 | 349 |
if (PIDE.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
|
350 |
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
|
351 |
delay_load.invoke() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
352 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
353 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
354 |
case msg: EditPaneUpdate |
60215 | 355 |
if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
356 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
357 |
msg.getWhat == EditPaneUpdate.CREATED || |
60215 | 358 |
msg.getWhat == EditPaneUpdate.DESTROYED => |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
359 |
val edit_pane = msg.getEditPane |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
360 |
val buffer = edit_pane.getBuffer |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
361 |
val text_area = edit_pane.getTextArea |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
362 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
363 |
if (buffer != null && text_area != null) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
364 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
365 |
msg.getWhat == EditPaneUpdate.CREATED) { |
50205 | 366 |
if (PIDE.session.is_ready) |
367 |
PIDE.init_view(buffer, text_area) |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
368 |
} |
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
|
369 |
else { |
53244 | 370 |
PIDE.dismissed_popups(text_area.getView) |
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
|
371 |
PIDE.exit_view(buffer, text_area) |
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
|
372 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
373 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
374 |
if (msg.getWhat == EditPaneUpdate.CREATED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
375 |
Completion_Popup.Text_Area.init(text_area) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
376 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
377 |
if (msg.getWhat == EditPaneUpdate.DESTROYED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
378 |
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
|
379 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
380 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
381 |
case msg: PropertiesChanged => |
62264
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
382 |
for { |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
383 |
view <- JEdit_Lib.jedit_views |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
384 |
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
|
385 |
} { |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
386 |
val buffer = edit_pane.getBuffer |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
387 |
val text_area = edit_pane.getTextArea |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
388 |
if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area) |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
389 |
} |
340f98836fd9
re-init document views for the sake of Text_Overview size;
wenzelm
parents:
62228
diff
changeset
|
390 |
|
56558
05c833d402bc
tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents:
56557
diff
changeset
|
391 |
PIDE.spell_checker.update(PIDE.options.value) |
52084
573e80625c78
more explicit Session.update_options as source of Global_Options event;
wenzelm
parents:
51616
diff
changeset
|
392 |
PIDE.session.update_options(PIDE.options.value) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
393 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
394 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
395 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
396 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
397 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
398 |
|
34618 | 399 |
override def start() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
400 |
{ |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
401 |
try { |
50709
985c081a4f11
disable search dialog pool on all platforms -- to prevent GUI synchronization problems seen on KDE (e.g. Kubuntu 12.10);
wenzelm
parents:
50566
diff
changeset
|
402 |
Debug.DISABLE_SEARCH_DIALOG_POOL = true |
985c081a4f11
disable search dialog pool on all platforms -- to prevent GUI synchronization problems seen on KDE (e.g. Kubuntu 12.10);
wenzelm
parents:
50566
diff
changeset
|
403 |
|
50205 | 404 |
PIDE.plugin = this |
62917
eed66ba99bd9
backout 930a30c1a9af: leads to odd effect of command-line options becoming persistent preferences;
wenzelm
parents:
62914
diff
changeset
|
405 |
PIDE.options.store(Options.init()) |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
406 |
PIDE.completion_history.load() |
56558
05c833d402bc
tuned signature -- explicit Spell_Checker_Variable;
wenzelm
parents:
56557
diff
changeset
|
407 |
PIDE.spell_checker.update(PIDE.options.value) |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
408 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
409 |
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
410 |
if (ModeProvider.instance.isInstanceOf[ModeProvider]) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
411 |
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
412 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
413 |
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
|
414 |
|
62973 | 415 |
val content = JEdit_Sessions.session_content(false) |
56801
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56775
diff
changeset
|
416 |
val resources = |
8dd9df88f647
some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
wenzelm
parents:
56775
diff
changeset
|
417 |
new JEdit_Resources(content.loaded_theories, content.known_theories, content.syntax) |
49524
68796a77c42b
Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
wenzelm
parents:
49523
diff
changeset
|
418 |
|
62051 | 419 |
PIDE.session.stop() |
56208 | 420 |
PIDE.session = new Session(resources) { |
50207 | 421 |
override def output_delay = PIDE.options.seconds("editor_output_delay") |
57867
abae8aff6262
added system option editor_output_delay: lower value might help big sessions under low-memory situations;
wenzelm
parents:
57680
diff
changeset
|
422 |
override def prune_delay = PIDE.options.seconds("editor_prune_delay") |
57974 | 423 |
override def syslog_limit = PIDE.options.int("editor_syslog_limit") |
50205 | 424 |
override def reparse_limit = PIDE.options.int("editor_reparse_limit") |
49288 | 425 |
} |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
426 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
427 |
PIDE.session.phase_changed += session_phase |
50205 | 428 |
PIDE.startup_failure = None |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
429 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
430 |
catch { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
431 |
case exn: Throwable => |
50205 | 432 |
PIDE.startup_failure = Some(exn) |
433 |
PIDE.startup_notified = false |
|
62228
6dfe5b12c5b2
report error on internal channel as well: startup_failure dialog may be too late;
wenzelm
parents:
62227
diff
changeset
|
434 |
Log.log(Log.ERROR, this, exn) |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
435 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
436 |
} |
34618 | 437 |
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
438 |
override def stop() |
34618 | 439 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
440 |
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
|
441 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
442 |
if (PIDE.startup_failure.isEmpty) { |
50205 | 443 |
PIDE.options.value.save_prefs() |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
444 |
PIDE.completion_history.value.save() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
445 |
} |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
446 |
|
56715
52125652e82a
clarified Session.Consumer, with Session.Outlet managed by dispatcher thread;
wenzelm
parents:
56662
diff
changeset
|
447 |
PIDE.session.phase_changed -= session_phase |
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
|
448 |
PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) |
50205 | 449 |
PIDE.session.stop() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
450 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
451 |
} |