author | wenzelm |
Fri, 07 Sep 2012 13:58:54 +0200 | |
changeset 49195 | 9d10bd85c1be |
parent 49101 | 21c8d2070be9 |
child 49245 | cb70157293c0 |
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 |
||
4 |
Main Isabelle/jEdit plugin setup. |
|
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 |
||
43520
cec9b95fa35d
explicit import java.lang.System to prevent odd scope problems;
wenzelm
parents:
43513
diff
changeset
|
12 |
import java.lang.System |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
import java.awt.Font |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
14 |
import javax.swing.JOptionPane |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
15 |
|
34497 | 16 |
import scala.collection.mutable |
44606 | 17 |
import scala.swing.{ComboBox, ListView, ScrollPane} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
18 |
|
39241 | 19 |
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, |
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
20 |
Buffer, EditPane, ServiceManager, View} |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
21 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
39043 | 22 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
43452
5cf548485529
avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;
wenzelm
parents:
43449
diff
changeset
|
23 |
import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider} |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
24 |
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} |
37068 | 25 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
34429 | 26 |
|
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
27 |
import org.gjt.sp.util.SyntaxUtilities |
39241 | 28 |
import org.gjt.sp.util.Log |
29 |
||
44721 | 30 |
import scala.actors.Actor._ |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
31 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
32 |
|
34618 | 33 |
object Isabelle |
34 |
{ |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
35 |
/* plugin instance */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
36 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
37 |
@volatile var startup_failure: Option[Throwable] = None |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
38 |
@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
|
39 |
|
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
40 |
@volatile var plugin: Plugin = null |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
41 |
@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
|
42 |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
43 |
def thy_load(): JEdit_Thy_Load = |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
44 |
session.thy_load.asInstanceOf[JEdit_Thy_Load] |
44955 | 45 |
|
48884
963b50ec6d73
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm
parents:
48872
diff
changeset
|
46 |
def get_recent_syntax(): Option[Outer_Syntax] = |
963b50ec6d73
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm
parents:
48872
diff
changeset
|
47 |
{ |
963b50ec6d73
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm
parents:
48872
diff
changeset
|
48 |
val current_session = session |
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
49 |
if (current_session.recent_syntax == Outer_Syntax.empty) None |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
50 |
else Some(current_session.recent_syntax) |
48884
963b50ec6d73
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm
parents:
48872
diff
changeset
|
51 |
} |
963b50ec6d73
clarified global get_recent_syntax: session always has its base_syntax, but it might be absent itself;
wenzelm
parents:
48872
diff
changeset
|
52 |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
53 |
|
34618 | 54 |
/* properties */ |
55 |
||
56 |
val OPTION_PREFIX = "options.isabelle." |
|
57 |
||
58 |
object Property |
|
59 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
60 |
def apply(name: String): String = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
61 |
jEdit.getProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
62 |
def apply(name: String, default: String): String = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
63 |
jEdit.getProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
64 |
def update(name: String, value: String) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
65 |
jEdit.setProperty(OPTION_PREFIX + name, value) |
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34463
diff
changeset
|
66 |
} |
34433 | 67 |
|
34618 | 68 |
object Boolean_Property |
69 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
70 |
def apply(name: String): Boolean = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
71 |
jEdit.getBooleanProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
72 |
def apply(name: String, default: Boolean): Boolean = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
73 |
jEdit.getBooleanProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
74 |
def update(name: String, value: Boolean) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
75 |
jEdit.setBooleanProperty(OPTION_PREFIX + name, value) |
34618 | 76 |
} |
77 |
||
78 |
object Int_Property |
|
79 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
80 |
def apply(name: String): Int = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
81 |
jEdit.getIntegerProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
82 |
def apply(name: String, default: Int): Int = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
83 |
jEdit.getIntegerProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
84 |
def update(name: String, value: Int) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
85 |
jEdit.setIntegerProperty(OPTION_PREFIX + name, value) |
34618 | 86 |
} |
87 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
88 |
object Double_Property |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
89 |
{ |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
90 |
def apply(name: String): Double = |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
91 |
jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0) |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
92 |
def apply(name: String, default: Double): Double = |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
93 |
jEdit.getDoubleProperty(OPTION_PREFIX + name, default) |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
94 |
def update(name: String, value: Double) = |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
95 |
jEdit.setDoubleProperty(OPTION_PREFIX + name, value) |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
96 |
} |
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
97 |
|
40850 | 98 |
object Time_Property |
99 |
{ |
|
100 |
def apply(name: String): Time = |
|
101 |
Time.seconds(Double_Property(name)) |
|
102 |
def apply(name: String, default: Time): Time = |
|
103 |
Time.seconds(Double_Property(name, default.seconds)) |
|
104 |
def update(name: String, value: Time) = |
|
105 |
Double_Property.update(name, value.seconds) |
|
106 |
} |
|
107 |
||
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
108 |
|
37164 | 109 |
/* font */ |
110 |
||
111 |
def font_family(): String = jEdit.getProperty("view.font") |
|
112 |
||
37019 | 113 |
def font_size(): Float = |
114 |
(jEdit.getIntegerProperty("view.fontsize", 16) * |
|
115 |
Int_Property("relative-font-size", 100)).toFloat / 100 |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
116 |
|
34618 | 117 |
|
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
118 |
/* tooltip markup */ |
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
119 |
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
120 |
def tooltip(text: String): String = |
37203
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
121 |
"<html><pre style=\"font-family: " + font_family() + "; font-size: " + |
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
122 |
Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) |
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
123 |
HTML.encode(text) + "</pre></html>" |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
124 |
|
44699
5199ee17c7d7
property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents:
44615
diff
changeset
|
125 |
private val tooltip_lb = Time.seconds(0.5) |
5199ee17c7d7
property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents:
44615
diff
changeset
|
126 |
private val tooltip_ub = Time.seconds(60.0) |
40849 | 127 |
def tooltip_dismiss_delay(): Time = |
44699
5199ee17c7d7
property "tooltip-dismiss-delay" is edited in ms, not seconds;
wenzelm
parents:
44615
diff
changeset
|
128 |
Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max tooltip_lb min tooltip_ub |
38854
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
129 |
|
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
130 |
def setup_tooltips() |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
131 |
{ |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
132 |
Swing_Thread.now { |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
133 |
val manager = javax.swing.ToolTipManager.sharedInstance |
40849 | 134 |
manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt) |
38854
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
135 |
} |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
136 |
} |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
137 |
|
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
138 |
|
39241 | 139 |
/* icons */ |
140 |
||
141 |
def load_icon(name: String): javax.swing.Icon = |
|
142 |
{ |
|
143 |
val icon = GUIUtilities.loadIcon(name) |
|
144 |
if (icon.getIconWidth < 0 || icon.getIconHeight < 0) |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
145 |
Log.log(Log.ERROR, icon, "Bad icon: " + name) |
39241 | 146 |
icon |
147 |
} |
|
148 |
||
149 |
||
44580
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
150 |
/* buffers */ |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
151 |
|
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
152 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
153 |
Swing_Thread.now { buffer_lock(buffer) { body } } |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
154 |
|
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
155 |
def buffer_text(buffer: JEditBuffer): String = |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
156 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
157 |
|
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
158 |
def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
159 |
|
48718 | 160 |
def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] = |
161 |
Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName)) |
|
162 |
||
163 |
def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] = |
|
164 |
{ |
|
165 |
val name = buffer_name(buffer) |
|
166 |
Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory)) |
|
167 |
} |
|
168 |
||
44580
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
169 |
|
38221 | 170 |
/* main jEdit components */ |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
171 |
|
37177 | 172 |
def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
173 |
|
44580
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
174 |
def jedit_buffer(name: String): Option[Buffer] = |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
175 |
jedit_buffers().find(buffer => buffer_name(buffer) == name) |
3bc9a215a56d
some support for hyperlinks between different buffers;
wenzelm
parents:
44577
diff
changeset
|
176 |
|
37177 | 177 |
def jedit_views(): Iterator[View] = jEdit.getViews().iterator |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
178 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
179 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
37177 | 180 |
view.getEditPanes().iterator.map(_.getTextArea) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
181 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
182 |
def jedit_text_areas(): Iterator[JEditTextArea] = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
183 |
jedit_views().flatMap(jedit_text_areas(_)) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
184 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
185 |
def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
186 |
jedit_text_areas().filter(_.getBuffer == buffer) |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
187 |
|
38843 | 188 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
38640 | 189 |
{ |
190 |
try { buffer.readLock(); body } |
|
191 |
finally { buffer.readUnlock() } |
|
192 |
} |
|
193 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
194 |
|
43449 | 195 |
/* document model and view */ |
196 |
||
197 |
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) |
|
198 |
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) |
|
199 |
||
44379 | 200 |
def document_views(buffer: Buffer): List[Document_View] = |
201 |
for { |
|
202 |
text_area <- jedit_text_areas(buffer).toList |
|
46997 | 203 |
doc_view = document_view(text_area) |
44379 | 204 |
if doc_view.isDefined |
205 |
} yield doc_view.get |
|
206 |
||
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
207 |
def exit_model(buffer: Buffer) |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
208 |
{ |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
209 |
swing_buffer_lock(buffer) { |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
210 |
jedit_text_areas(buffer).foreach(Document_View.exit) |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
211 |
Document_Model.exit(buffer) |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
212 |
} |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
213 |
} |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
214 |
|
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
|
215 |
def init_model(buffer: Buffer) |
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
|
216 |
{ |
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
|
217 |
swing_buffer_lock(buffer) { |
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
|
218 |
val opt_model = |
48717
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
48709
diff
changeset
|
219 |
buffer_node_name(buffer) match { |
622251b2b0f1
clarified Sidekick configuration, including minor modes;
wenzelm
parents:
48709
diff
changeset
|
220 |
case Some(node_name) => |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
221 |
document_model(buffer) match { |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
222 |
case Some(model) if model.name == node_name => Some(model) |
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
223 |
case _ => Some(Document_Model.init(session, buffer, node_name)) |
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
|
224 |
} |
47058
34761733526c
refined init_model: allow change of buffer name as caused by "Save as", for example;
wenzelm
parents:
46997
diff
changeset
|
225 |
case None => 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
|
226 |
} |
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
|
227 |
if (opt_model.isDefined) { |
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
|
228 |
for (text_area <- jedit_text_areas(buffer)) { |
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
|
229 |
if (document_view(text_area).map(_.model) != opt_model) |
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
|
230 |
Document_View.init(opt_model.get, 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
|
231 |
} |
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
|
232 |
} |
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
|
233 |
} |
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
|
234 |
} |
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
|
235 |
|
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
|
236 |
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
|
237 |
{ |
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
|
238 |
swing_buffer_lock(buffer) { |
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
|
239 |
document_model(buffer) match { |
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
|
240 |
case Some(model) => Document_View.init(model, 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
|
241 |
case None => |
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
|
242 |
} |
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
|
243 |
} |
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
|
244 |
} |
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
|
245 |
|
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 |
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
|
247 |
{ |
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
|
248 |
swing_buffer_lock(buffer) { |
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
|
249 |
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
|
250 |
} |
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
|
251 |
} |
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
|
252 |
|
43449 | 253 |
|
37068 | 254 |
/* dockable windows */ |
255 |
||
256 |
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
257 |
||
39515 | 258 |
def docked_session(view: View): Option[Session_Dockable] = |
259 |
wm(view).getDockableWindow("isabelle-session") match { |
|
260 |
case dockable: Session_Dockable => Some(dockable) |
|
261 |
case _ => None |
|
262 |
} |
|
263 |
||
37068 | 264 |
def docked_output(view: View): Option[Output_Dockable] = |
265 |
wm(view).getDockableWindow("isabelle-output") match { |
|
266 |
case dockable: Output_Dockable => Some(dockable) |
|
267 |
case _ => None |
|
268 |
} |
|
269 |
||
270 |
def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
271 |
wm(view).getDockableWindow("isabelle-raw-output") match { |
|
272 |
case dockable: Raw_Output_Dockable => Some(dockable) |
|
273 |
case _ => None |
|
274 |
} |
|
275 |
||
276 |
def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
277 |
wm(view).getDockableWindow("isabelle-protocol") match { |
|
278 |
case dockable: Protocol_Dockable => Some(dockable) |
|
279 |
case _ => None |
|
280 |
} |
|
281 |
||
282 |
||
39517 | 283 |
/* logic image */ |
284 |
||
285 |
def default_logic(): String = |
|
286 |
{ |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
287 |
val logic = Isabelle_System.getenv("JEDIT_LOGIC") |
39517 | 288 |
if (logic != "") logic |
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
289 |
else Isabelle_System.getenv_strict("ISABELLE_LOGIC") |
39517 | 290 |
} |
291 |
||
292 |
class Logic_Entry(val name: String, val description: String) |
|
293 |
{ |
|
294 |
override def toString = description |
|
295 |
} |
|
296 |
||
297 |
def logic_selector(logic: String): ComboBox[Logic_Entry] = |
|
298 |
{ |
|
299 |
val entries = |
|
300 |
new Logic_Entry("", "default (" + default_logic() + ")") :: |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
301 |
Isabelle_System.find_logics().map(name => new Logic_Entry(name, name)) |
39517 | 302 |
val component = new ComboBox(entries) |
303 |
entries.find(_.name == logic) match { |
|
304 |
case None => |
|
305 |
case Some(entry) => component.selection.item = entry |
|
306 |
} |
|
39702 | 307 |
component.tooltip = "Isabelle logic image" |
39517 | 308 |
component |
309 |
} |
|
39702 | 310 |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
311 |
def session_args(): List[String] = |
39702 | 312 |
{ |
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43661
diff
changeset
|
313 |
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _) |
39702 | 314 |
val logic = { |
315 |
val logic = Property("logic") |
|
316 |
if (logic != null && logic != "") logic |
|
317 |
else Isabelle.default_logic() |
|
318 |
} |
|
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
319 |
modes ::: List(logic) |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
320 |
} |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
321 |
|
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48884
diff
changeset
|
322 |
def session_content(inlined_files: Boolean): Build.Session_Content = |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
323 |
{ |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
324 |
val dirs = Path.split(Isabelle_System.getenv("JEDIT_SESSION_DIRS")) |
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
325 |
val name = Path.explode(session_args().last).base.implode // FIXME more robust |
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48884
diff
changeset
|
326 |
Build.session_content(inlined_files, dirs, name).check_errors |
39702 | 327 |
} |
44238
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
328 |
|
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
329 |
|
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
330 |
/* convenience actions */ |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
331 |
|
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
332 |
private def user_input(text_area: JEditTextArea, s1: String, s2: String = "") |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
333 |
{ |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
334 |
s1.foreach(text_area.userInput(_)) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
335 |
s2.foreach(text_area.userInput(_)) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
336 |
s2.foreach(_ => text_area.goToPrevCharacter(false)) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
337 |
} |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
338 |
|
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
339 |
def input_sub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sub_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
340 |
def input_sup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.sup_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
341 |
def input_isub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isub_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
342 |
def input_isup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.isup_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
343 |
def input_bsub(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsub_decoded, Symbol.esub_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
344 |
def input_bsup(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bsup_decoded, Symbol.esup_decoded) |
36120feb70ed
some convenience actions/shortcuts for control symbols;
wenzelm
parents:
44225
diff
changeset
|
345 |
def input_bold(text_area: JEditTextArea): Unit = user_input(text_area, Symbol.bold_decoded) |
44864
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
346 |
|
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
347 |
def check_buffer(buffer: Buffer) |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
348 |
{ |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
349 |
document_model(buffer) match { |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
350 |
case None => |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
351 |
case Some(model) => model.full_perspective() |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
352 |
} |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
353 |
} |
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
354 |
|
e50557cb0eb6
explicit jEdit actions -- to enable key mappings, for example;
wenzelm
parents:
44721
diff
changeset
|
355 |
def cancel_execution() { session.cancel_execution() } |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
356 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
357 |
|
34429 | 358 |
|
34618 | 359 |
class Plugin extends EBPlugin |
360 |
{ |
|
44577
96b6388d06c4
separate module for jEdit primitives for loading theory files;
wenzelm
parents:
44574
diff
changeset
|
361 |
/* theory files */ |
44574 | 362 |
|
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
363 |
private lazy val delay_load = |
44574 | 364 |
Swing_Thread.delay_last(Isabelle.session.load_delay) |
365 |
{ |
|
44963
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44955
diff
changeset
|
366 |
val view = jEdit.getActiveView() |
4662dddc2fd8
explicit check_file wrt. jEdit VFS, to avoid slightly confusing empty buffer after IO error;
wenzelm
parents:
44955
diff
changeset
|
367 |
|
44574 | 368 |
val buffers = Isabelle.jedit_buffers().toList |
46761 | 369 |
if (buffers.forall(_.isLoaded)) { |
370 |
def loaded_buffer(name: String): Boolean = |
|
371 |
buffers.exists(buffer => Isabelle.buffer_name(buffer) == name) |
|
44574 | 372 |
|
46761 | 373 |
val thys = |
374 |
for (buffer <- buffers; model <- Isabelle.document_model(buffer)) |
|
375 |
yield model.name |
|
376 |
||
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
377 |
val thy_info = new Thy_Info(Isabelle.thy_load) |
46761 | 378 |
// FIXME avoid I/O in Swing thread!?! |
49098
673e0ed547af
bypass slow check for inlined files, where it is not really required;
wenzelm
parents:
48884
diff
changeset
|
379 |
val files = thy_info.dependencies(true, thys).deps.map(_._1.node). |
46761 | 380 |
filter(file => !loaded_buffer(file) && Isabelle.thy_load.check_file(view, file)) |
44574 | 381 |
|
46761 | 382 |
if (!files.isEmpty) { |
383 |
val files_list = new ListView(files.sorted) |
|
384 |
for (i <- 0 until files.length) |
|
385 |
files_list.selection.indices += i |
|
44606 | 386 |
|
46761 | 387 |
val answer = |
388 |
Library.confirm_dialog(view, |
|
389 |
"Auto loading of required files", |
|
390 |
JOptionPane.YES_NO_OPTION, |
|
391 |
"The following files are required to resolve theory imports.", |
|
392 |
"Reload selected files now?", |
|
393 |
new ScrollPane(files_list)) |
|
394 |
if (answer == 0) { |
|
395 |
files.foreach(file => |
|
396 |
if (files_list.selection.items.contains(file)) |
|
397 |
jEdit.openFile(null: View, file)) |
|
398 |
} |
|
399 |
} |
|
44606 | 400 |
} |
44574 | 401 |
} |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
402 |
|
44574 | 403 |
|
404 |
/* session manager */ |
|
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
405 |
|
39633 | 406 |
private val session_manager = actor { |
407 |
loop { |
|
408 |
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
|
409 |
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
|
410 |
phase match { |
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
|
411 |
case Session.Failed => |
46918
1752164d916b
prefer asynchronous context switch from actor to swing thread, to reduce danger of deadlocks;
wenzelm
parents:
46771
diff
changeset
|
412 |
Swing_Thread.later { |
48022 | 413 |
Library.error_dialog(jEdit.getActiveView, "Prover process failure", |
414 |
"Isabelle Syslog", Library.scrollable_text(Isabelle.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
|
415 |
} |
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
|
416 |
|
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
417 |
case Session.Ready => |
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
418 |
Isabelle.jedit_buffers.foreach(Isabelle.init_model) |
49195 | 419 |
Swing_Thread.later { delay_load.invoke() } |
44573
51f8895b9ad9
some dialog for auto loading of required files (still inactive);
wenzelm
parents:
44434
diff
changeset
|
420 |
|
46740
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
421 |
case Session.Shutdown => |
852baa599351
explicitly revoke delay, to avoid spurious timer events after deactivation of related components;
wenzelm
parents:
46204
diff
changeset
|
422 |
Isabelle.jedit_buffers.foreach(Isabelle.exit_model) |
49195 | 423 |
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
|
424 |
|
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
|
425 |
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
|
426 |
} |
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
|
427 |
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
|
428 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
429 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
430 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
431 |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
432 |
|
34618 | 433 |
/* main plugin plumbing */ |
34433 | 434 |
|
34767 | 435 |
override def handleMessage(message: EBMessage) |
34618 | 436 |
{ |
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
|
437 |
Swing_Thread.assert() |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
438 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
439 |
if (Isabelle.startup_failure.isDefined && !Isabelle.startup_notified) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
440 |
message match { |
49100
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
441 |
case msg: EditorStarted => |
e7aecf2a5fc4
prefer old startup dialog scheme (cf. 514bb82514df);
wenzelm
parents:
49099
diff
changeset
|
442 |
Library.error_dialog(null, "Isabelle plugin startup failure", |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
443 |
Library.scrollable_text(Exn.message(Isabelle.startup_failure.get)), |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
444 |
"Prover IDE inactive!") |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
445 |
Isabelle.startup_notified = true |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
446 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
447 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
448 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
449 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
450 |
if (Isabelle.startup_failure.isEmpty) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
451 |
message match { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
452 |
case msg: EditorStarted => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
453 |
if (Isabelle.Boolean_Property("auto-start")) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
454 |
Isabelle.session.start(Isabelle.session_args()) |
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37241
diff
changeset
|
455 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
456 |
case msg: BufferUpdate |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
457 |
if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
458 |
if (Isabelle.session.is_ready) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
459 |
val buffer = msg.getBuffer |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
460 |
if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer) |
49195 | 461 |
Swing_Thread.later { delay_load.invoke() } |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
462 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
463 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
464 |
case msg: EditPaneUpdate |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
465 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
466 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
467 |
msg.getWhat == EditPaneUpdate.CREATED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
468 |
msg.getWhat == EditPaneUpdate.DESTROYED) => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
469 |
val edit_pane = msg.getEditPane |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
470 |
val buffer = edit_pane.getBuffer |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
471 |
val text_area = edit_pane.getTextArea |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
472 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
473 |
if (buffer != null && text_area != null) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
474 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
475 |
msg.getWhat == EditPaneUpdate.CREATED) { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
476 |
if (Isabelle.session.is_ready) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
477 |
Isabelle.init_view(buffer, text_area) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
478 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
479 |
else Isabelle.exit_view(buffer, 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
|
480 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
481 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
482 |
case msg: PropertiesChanged => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
483 |
Isabelle.setup_tooltips() |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
484 |
Isabelle.session.global_settings.event(Session.Global_Settings) |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
485 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
486 |
case _ => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
487 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
488 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
489 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
490 |
|
34618 | 491 |
override def start() |
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
492 |
{ |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
493 |
try { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
494 |
Isabelle.plugin = this |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
495 |
Isabelle.setup_tooltips() |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
496 |
Isabelle_System.init() |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
497 |
Isabelle_System.install_fonts() |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
498 |
|
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
499 |
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
500 |
if (ModeProvider.instance.isInstanceOf[ModeProvider]) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
501 |
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
502 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
503 |
val content = Isabelle.session_content(false) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
504 |
val thy_load = new JEdit_Thy_Load(content.loaded_theories, content.syntax) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
505 |
Isabelle.session = new Session(thy_load) |
48870
4accee106f0f
clarified initialization of Thy_Load, Thy_Info, Session;
wenzelm
parents:
48791
diff
changeset
|
506 |
|
49099
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
507 |
Isabelle.session.phase_changed += session_manager |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
508 |
Isabelle.startup_failure = None |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
509 |
} |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
510 |
catch { |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
511 |
case exn: Throwable => |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
512 |
Isabelle.startup_failure = Some(exn) |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
513 |
Isabelle.startup_notified = false |
10e899bb6530
more permissive handling of plugin startup failure;
wenzelm
parents:
49098
diff
changeset
|
514 |
} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
515 |
} |
34618 | 516 |
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
517 |
override def stop() |
34618 | 518 |
{ |
49101
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
519 |
Isabelle.session.phase_changed -= session_manager |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
520 |
Isabelle.jedit_buffers.foreach(Isabelle.exit_model) |
21c8d2070be9
continue with more robust dummy session after failed startup;
wenzelm
parents:
49100
diff
changeset
|
521 |
Isabelle.session.stop() |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
522 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
523 |
} |