author | wenzelm |
Thu, 20 Feb 2014 14:36:17 +0100 | |
changeset 55618 | 995162143ef4 |
parent 55490 | 9b0fb0e2c9f5 |
child 55621 | 8d69c15b6fb9 |
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 |
|
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
|
16 |
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug} |
53487 | 17 |
import org.jedit.options.CombinedOptions |
18 |
import org.gjt.sp.jedit.gui.AboutDialog |
|
39043 | 19 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
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} |
34429 | 22 |
|
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
23 |
import org.gjt.sp.util.SyntaxUtilities |
39241 | 24 |
|
44721 | 25 |
import scala.actors.Actor._ |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
26 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
27 |
|
50205 | 28 |
object PIDE |
34618 | 29 |
{ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
30 |
/* plugin instance */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
31 |
|
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
32 |
val options = new JEdit_Options |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
33 |
val completion_history = new Completion.History_Variable |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
34 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
35 |
@volatile var startup_failure: Option[Throwable] = None |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
36 |
@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
|
37 |
|
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
38 |
@volatile var plugin: Plugin = null |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
39 |
@volatile var session: Session = new Session(new JEdit_Thy_Load(Set.empty, Outer_Syntax.empty)) |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
40 |
|
53074 | 41 |
def options_changed() { |
42 |
session.global_options.event(Session.Global_Options(options.value)) |
|
43 |
plugin.load_theories() |
|
44 |
} |
|
52815
eaad5fe7bb1b
actions and shortcuts to change node_required status, with painter that looks like CheckBox (non-clickable);
wenzelm
parents:
52807
diff
changeset
|
45 |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
46 |
def thy_load(): JEdit_Thy_Load = |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
47 |
session.thy_load.asInstanceOf[JEdit_Thy_Load] |
44955 | 48 |
|
52971
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52876
diff
changeset
|
49 |
lazy val editor = new JEdit_Editor |
31926d2c04ee
tuned signature -- more abstract PIDE editor operations;
wenzelm
parents:
52876
diff
changeset
|
50 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
51 |
|
53244 | 52 |
/* popups */ |
53 |
||
54 |
def dismissed_popups(view: View): Boolean = |
|
55 |
{ |
|
53272 | 56 |
var dismissed = false |
57 |
||
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
58 |
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
|
59 |
if (Completion_Popup.Text_Area.dismissed(text_area)) dismissed = true) |
53272 | 60 |
|
61 |
if (Pretty_Tooltip.dismissed_all()) dismissed = true |
|
62 |
||
63 |
dismissed |
|
53244 | 64 |
} |
65 |
||
66 |
||
43449 | 67 |
/* document model and view */ |
68 |
||
69 |
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
70 |
|
43449 | 71 |
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) |
72 |
||
44379 | 73 |
def document_views(buffer: Buffer): List[Document_View] = |
74 |
for { |
|
49406 | 75 |
text_area <- JEdit_Lib.jedit_text_areas(buffer).toList |
54529 | 76 |
doc_view <- document_view(text_area) |
77 |
} yield doc_view |
|
44379 | 78 |
|
54522 | 79 |
def document_models(): List[Document_Model] = |
80 |
for { |
|
81 |
buffer <- JEdit_Lib.jedit_buffers().toList |
|
82 |
model <- document_model(buffer) |
|
83 |
} yield model |
|
84 |
||
85 |
def document_blobs(): Document.Blobs = |
|
86 |
document_models().filterNot(_.is_theory).map(model => (model.node_name -> model.blob())).toMap |
|
87 |
||
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
|
88 |
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
|
89 |
{ |
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
|
90 |
Swing_Thread.now { |
54461 | 91 |
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
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
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
|
96 |
}) |
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
|
97 |
} |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
98 |
} |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
99 |
|
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
|
100 |
def init_models(buffers: List[Buffer]) |
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
|
101 |
{ |
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
|
102 |
Swing_Thread.now { |
54461 | 103 |
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
|
104 |
val init_edits = |
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
|
105 |
(List.empty[Document.Edit_Text] /: buffers) { case (edits, 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
|
106 |
JEdit_Lib.buffer_lock(buffer) { |
54561
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
107 |
if (buffer.getBooleanProperty(Buffer.GZIPPED)) edits |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
108 |
else { |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
109 |
val node_name = thy_load.node_name(buffer) |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
110 |
val (model_edits, model) = |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
111 |
document_model(buffer) match { |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
112 |
case Some(model) if model.node_name == node_name => (Nil, model) |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
113 |
case _ => |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
114 |
val model = Document_Model.init(session, buffer, node_name) |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
115 |
(model.init_edits(), model) |
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
116 |
} |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
117 |
for { |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
118 |
text_area <- JEdit_Lib.jedit_text_areas(buffer) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
119 |
if document_view(text_area).map(_.model) != Some(model) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
120 |
} Document_View.init(model, text_area) |
54561
ceb190f4f69f
exclude gzipped files from document model, to avoid confusion about actual file name and content;
wenzelm
parents:
54529
diff
changeset
|
121 |
model_edits ::: edits |
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
|
122 |
} |
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
|
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 |
} |
54522 | 125 |
session.update(document_blobs(), init_edits) |
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
|
126 |
} |
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
|
127 |
} |
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
|
128 |
|
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 |
def init_view(buffer: Buffer, text_area: JEditTextArea) |
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 |
{ |
49406 | 131 |
JEdit_Lib.swing_buffer_lock(buffer) { |
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
|
132 |
document_model(buffer) match { |
55432
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
133 |
case Some(model) => Document_View.init(model, text_area) |
9c53198dbb1c
maintain multiple command chunks and markup trees: for main chunk and loaded files;
wenzelm
parents:
54561
diff
changeset
|
134 |
case None => |
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
|
135 |
} |
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
|
136 |
} |
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
|
137 |
} |
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
|
138 |
|
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 |
def exit_view(buffer: Buffer, text_area: JEditTextArea) |
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 |
{ |
49406 | 141 |
JEdit_Lib.swing_buffer_lock(buffer) { |
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
|
142 |
Document_View.exit(text_area) |
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
|
143 |
} |
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
|
144 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
145 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
146 |
|
34429 | 147 |
|
34618 | 148 |
class Plugin extends EBPlugin |
149 |
{ |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
150 |
/* theory files */ |
44574 | 151 |
|
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
|
152 |
private lazy val delay_init = |
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
|
153 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) |
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
|
154 |
{ |
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
|
155 |
PIDE.init_models(JEdit_Lib.jedit_buffers().toList) |
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
|
156 |
} |
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
|
157 |
|
53074 | 158 |
def load_theories() { Swing_Thread.later { delay_load.invoke() }} |
159 |
||
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
160 |
private lazy val delay_load = |
50207 | 161 |
Swing_Thread.delay_last(PIDE.options.seconds("editor_load_delay")) |
44574 | 162 |
{ |
53074 | 163 |
if (Isabelle.continuous_checking) { |
164 |
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
|
165 |
|
53074 | 166 |
val buffers = JEdit_Lib.jedit_buffers().toList |
167 |
if (buffers.forall(_.isLoaded)) { |
|
168 |
def loaded_buffer(name: String): Boolean = |
|
169 |
buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name) |
|
44574 | 170 |
|
53074 | 171 |
val thys = |
54509
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54461
diff
changeset
|
172 |
for { |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54461
diff
changeset
|
173 |
buffer <- buffers |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54461
diff
changeset
|
174 |
model <- PIDE.document_model(buffer) |
1f77110c94ef
maintain document model for all files, with document view for theory only, and special blob for non-theory files;
wenzelm
parents:
54461
diff
changeset
|
175 |
if model.is_theory |
55490 | 176 |
} yield (model.node_name, Position.none) |
46761 | 177 |
|
53074 | 178 |
val thy_info = new Thy_Info(PIDE.thy_load) |
179 |
// FIXME avoid I/O in Swing thread!?! |
|
180 |
val files = thy_info.dependencies(thys).deps.map(_.name.node). |
|
181 |
filter(file => !loaded_buffer(file) && PIDE.thy_load.check_file(view, file)) |
|
44574 | 182 |
|
53074 | 183 |
if (!files.isEmpty) { |
53715 | 184 |
if (PIDE.options.bool("jedit_auto_load")) { |
185 |
files.foreach(file => jEdit.openFile(null: View, file)) |
|
186 |
} |
|
187 |
else { |
|
188 |
val files_list = new ListView(files.sorted) |
|
189 |
for (i <- 0 until files.length) |
|
190 |
files_list.selection.indices += i |
|
44606 | 191 |
|
53715 | 192 |
val answer = |
193 |
GUI.confirm_dialog(view, |
|
194 |
"Auto loading of required files", |
|
195 |
JOptionPane.YES_NO_OPTION, |
|
196 |
"The following files are required to resolve theory imports.", |
|
197 |
"Reload selected files now?", |
|
198 |
new ScrollPane(files_list), |
|
199 |
new Isabelle.Continuous_Checking) |
|
200 |
if (answer == 0) { |
|
201 |
files.foreach(file => |
|
202 |
if (files_list.selection.items.contains(file)) |
|
203 |
jEdit.openFile(null: View, file)) |
|
204 |
} |
|
53074 | 205 |
} |
46761 | 206 |
} |
207 |
} |
|
44606 | 208 |
} |
44574 | 209 |
} |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
210 |
|
44574 | 211 |
|
212 |
/* session manager */ |
|
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
213 |
|
39633 | 214 |
private val session_manager = actor { |
215 |
loop { |
|
216 |
react { |
|
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
|
217 |
case phase: Session.Phase => |
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
|
218 |
phase match { |
50808
1702ed63c2db
more general prover termination dialog, which might indicate undetected failure or just ML "exit 0";
wenzelm
parents:
50709
diff
changeset
|
219 |
case Session.Inactive | Session.Failed => |
46918
1752164d916b
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents:
46771
diff
changeset
|
220 |
Swing_Thread.later { |
51616 | 221 |
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated", |
222 |
"Isabelle Syslog", GUI.scrollable_text(PIDE.session.current_syslog())) |
|
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
|
223 |
} |
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
|
224 |
|
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
225 |
case Session.Ready => |
52084
573e80625c78
more explicit Session.update_options as source of Global_Options event;
wenzelm
parents:
51616
diff
changeset
|
226 |
PIDE.session.update_options(PIDE.options.value) |
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
|
227 |
PIDE.init_models(JEdit_Lib.jedit_buffers().toList) |
49195 | 228 |
Swing_Thread.later { delay_load.invoke() } |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
229 |
|
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
230 |
case Session.Shutdown => |
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
|
231 |
PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) |
49195 | 232 |
Swing_Thread.later { delay_load.revoke() } |
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
233 |
|
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
|
234 |
case _ => |
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
|
235 |
} |
55618 | 236 |
case bad => System.err.println("session_manager: ignoring bad message " + bad) |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
237 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
238 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
239 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
240 |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
241 |
|
34618 | 242 |
/* main plugin plumbing */ |
34433 | 243 |
|
34767 | 244 |
override def handleMessage(message: EBMessage) |
34618 | 245 |
{ |
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
|
246 |
Swing_Thread.assert() |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
247 |
|
50205 | 248 |
if (PIDE.startup_failure.isDefined && !PIDE.startup_notified) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
249 |
message match { |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
250 |
case msg: EditorStarted => |
51616 | 251 |
GUI.error_dialog(null, "Isabelle plugin startup failure", |
252 |
GUI.scrollable_text(Exn.message(PIDE.startup_failure.get)), |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
253 |
"Prover IDE inactive!") |
50205 | 254 |
PIDE.startup_notified = true |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
255 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
256 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
257 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
258 |
|
50205 | 259 |
if (PIDE.startup_failure.isEmpty) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
260 |
message match { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
261 |
case msg: EditorStarted => |
50408
1fac4ff86381
discontinued option jedit_auto_start, which is somewhat pointless as there is no manual session start within Isabelle/jEdit;
wenzelm
parents:
50363
diff
changeset
|
262 |
PIDE.session.start(Isabelle_Logic.session_args()) |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37241
diff
changeset
|
263 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
264 |
case msg: BufferUpdate |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
265 |
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => |
50205 | 266 |
if (PIDE.session.is_ready) { |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
267 |
val buffer = msg.getBuffer |
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
|
268 |
if (buffer != null && !buffer.isLoading) delay_init.invoke() |
53074 | 269 |
load_theories() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
270 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
271 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
272 |
case msg: EditPaneUpdate |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
273 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
274 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
275 |
msg.getWhat == EditPaneUpdate.CREATED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
276 |
msg.getWhat == EditPaneUpdate.DESTROYED) => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
277 |
val edit_pane = msg.getEditPane |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
278 |
val buffer = edit_pane.getBuffer |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
279 |
val text_area = edit_pane.getTextArea |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
280 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
281 |
if (buffer != null && text_area != null) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
282 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
283 |
msg.getWhat == EditPaneUpdate.CREATED) { |
50205 | 284 |
if (PIDE.session.is_ready) |
285 |
PIDE.init_view(buffer, text_area) |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
286 |
} |
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
|
287 |
else { |
53244 | 288 |
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
|
289 |
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
|
290 |
} |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
291 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
292 |
if (msg.getWhat == EditPaneUpdate.CREATED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
293 |
Completion_Popup.Text_Area.init(text_area) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
294 |
|
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
295 |
if (msg.getWhat == EditPaneUpdate.DESTROYED) |
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
296 |
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
|
297 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
298 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
299 |
case msg: PropertiesChanged => |
52084
573e80625c78
more explicit Session.update_options as source of Global_Options event;
wenzelm
parents:
51616
diff
changeset
|
300 |
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
|
301 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
302 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
303 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
304 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
305 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
306 |
|
34618 | 307 |
override def start() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
308 |
{ |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
309 |
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
|
310 |
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
|
311 |
|
50205 | 312 |
PIDE.plugin = this |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
313 |
Isabelle_System.init() |
51614
22d1dd43f089
separate module Isabelle_Font, to keep this out of the way of generic Isabelle_System operations, notably for non-Isabelle/jEdit applications;
wenzelm
parents:
51294
diff
changeset
|
314 |
Isabelle_Font.install_fonts() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
315 |
|
53338 | 316 |
PIDE.options.update(Options.init()) |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
317 |
PIDE.completion_history.load() |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
318 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
319 |
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
320 |
if (ModeProvider.instance.isInstanceOf[ModeProvider]) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
321 |
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
322 |
|
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
323 |
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
|
324 |
|
49246 | 325 |
val content = Isabelle_Logic.session_content(false) |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
326 |
val thy_load = new JEdit_Thy_Load(content.loaded_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
|
327 |
|
50205 | 328 |
PIDE.session = new Session(thy_load) { |
50207 | 329 |
override def output_delay = PIDE.options.seconds("editor_output_delay") |
50205 | 330 |
override def reparse_limit = PIDE.options.int("editor_reparse_limit") |
49288 | 331 |
} |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
332 |
|
50205 | 333 |
PIDE.session.phase_changed += session_manager |
334 |
PIDE.startup_failure = None |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
335 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
336 |
catch { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
337 |
case exn: Throwable => |
50205 | 338 |
PIDE.startup_failure = Some(exn) |
339 |
PIDE.startup_notified = false |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
340 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
341 |
} |
34618 | 342 |
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
343 |
override def stop() |
34618 | 344 |
{ |
53274
1760c01f1c78
maintain Completion_Popup.Text_Area as client property like Document_View;
wenzelm
parents:
53272
diff
changeset
|
345 |
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
|
346 |
|
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
347 |
if (PIDE.startup_failure.isEmpty) { |
50205 | 348 |
PIDE.options.value.save_prefs() |
53337
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
349 |
PIDE.completion_history.value.save() |
b3817a0e3211
sort items according to persistent history of frequency of use;
wenzelm
parents:
53277
diff
changeset
|
350 |
} |
49245
cb70157293c0
manage Isabelle/jEdit options as Isabelle/Scala options (with persistent preferences);
wenzelm
parents:
49195
diff
changeset
|
351 |
|
50205 | 352 |
PIDE.session.phase_changed -= session_manager |
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
|
353 |
PIDE.exit_models(JEdit_Lib.jedit_buffers().toList) |
50205 | 354 |
PIDE.session.stop() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
355 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
356 |
} |