| author | wenzelm |
| Tue, 16 Aug 2011 22:48:31 +0200 | |
| changeset 44225 | a8f921e6484f |
| parent 44222 | 9d5ef6cd4ee1 |
| child 44238 | 36120feb70ed |
| 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 |
| 43645 | 13 |
import java.io.{File, FileInputStream, IOException}
|
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
import java.awt.Font |
|
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 |
| 39517 | 17 |
import scala.swing.ComboBox |
|
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,
|
| 43645 | 20 |
Buffer, EditPane, MiscUtilities, 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}
|
| 39633 | 24 |
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
|
| 37068 | 25 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
26 |
import org.gjt.sp.jedit.io.{VFS, FileVFS, VFSManager}
|
| 34429 | 27 |
|
|
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
28 |
import org.gjt.sp.util.SyntaxUtilities |
| 39241 | 29 |
import org.gjt.sp.util.Log |
30 |
||
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
31 |
import scala.actors.Actor |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
32 |
import Actor._ |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
33 |
|
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
34 |
|
| 34618 | 35 |
object Isabelle |
36 |
{
|
|
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
37 |
/* plugin instance */ |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
38 |
|
|
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
39 |
var plugin: Plugin = null |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
40 |
var session: Session = null |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
41 |
|
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
42 |
|
| 34618 | 43 |
/* properties */ |
44 |
||
45 |
val OPTION_PREFIX = "options.isabelle." |
|
46 |
||
47 |
object Property |
|
48 |
{
|
|
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
49 |
def apply(name: String): String = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
50 |
jEdit.getProperty(OPTION_PREFIX + name) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
51 |
def apply(name: String, default: String): String = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
52 |
jEdit.getProperty(OPTION_PREFIX + name, default) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
53 |
def update(name: String, value: String) = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
54 |
jEdit.setProperty(OPTION_PREFIX + name, value) |
|
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34463
diff
changeset
|
55 |
} |
| 34433 | 56 |
|
| 34618 | 57 |
object Boolean_Property |
58 |
{
|
|
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
59 |
def apply(name: String): Boolean = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
60 |
jEdit.getBooleanProperty(OPTION_PREFIX + name) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
61 |
def apply(name: String, default: Boolean): Boolean = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
62 |
jEdit.getBooleanProperty(OPTION_PREFIX + name, default) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
63 |
def update(name: String, value: Boolean) = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
64 |
jEdit.setBooleanProperty(OPTION_PREFIX + name, value) |
| 34618 | 65 |
} |
66 |
||
67 |
object Int_Property |
|
68 |
{
|
|
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
69 |
def apply(name: String): Int = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
70 |
jEdit.getIntegerProperty(OPTION_PREFIX + name) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
71 |
def apply(name: String, default: Int): Int = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
72 |
jEdit.getIntegerProperty(OPTION_PREFIX + name, default) |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
73 |
def update(name: String, value: Int) = |
|
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
74 |
jEdit.setIntegerProperty(OPTION_PREFIX + name, value) |
| 34618 | 75 |
} |
76 |
||
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
77 |
object Double_Property |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
78 |
{
|
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
79 |
def apply(name: String): Double = |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
80 |
jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0) |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
81 |
def apply(name: String, default: Double): Double = |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
82 |
jEdit.getDoubleProperty(OPTION_PREFIX + name, default) |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
83 |
def update(name: String, value: Double) = |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
84 |
jEdit.setDoubleProperty(OPTION_PREFIX + name, value) |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
85 |
} |
|
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
86 |
|
| 40850 | 87 |
object Time_Property |
88 |
{
|
|
89 |
def apply(name: String): Time = |
|
90 |
Time.seconds(Double_Property(name)) |
|
91 |
def apply(name: String, default: Time): Time = |
|
92 |
Time.seconds(Double_Property(name, default.seconds)) |
|
93 |
def update(name: String, value: Time) = |
|
94 |
Double_Property.update(name, value.seconds) |
|
95 |
} |
|
96 |
||
|
40848
8662b9b1f123
more abstract/uniform handling of time, preferring seconds as Double;
wenzelm
parents:
40474
diff
changeset
|
97 |
|
| 37164 | 98 |
/* font */ |
99 |
||
100 |
def font_family(): String = jEdit.getProperty("view.font")
|
|
101 |
||
| 37019 | 102 |
def font_size(): Float = |
103 |
(jEdit.getIntegerProperty("view.fontsize", 16) *
|
|
104 |
Int_Property("relative-font-size", 100)).toFloat / 100
|
|
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
105 |
|
| 34618 | 106 |
|
| 39043 | 107 |
/* text area ranges */ |
108 |
||
| 43714 | 109 |
sealed case class Gfx_Range(val x: Int, val y: Int, val length: Int) |
| 39043 | 110 |
|
111 |
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
112 |
{
|
|
113 |
val p = text_area.offsetToXY(range.start) |
|
114 |
val q = text_area.offsetToXY(range.stop) |
|
115 |
if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) |
|
116 |
else None |
|
117 |
} |
|
118 |
||
119 |
||
|
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
120 |
/* tooltip markup */ |
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
121 |
|
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
122 |
def tooltip(text: String): String = |
|
37203
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
123 |
"<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
|
124 |
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
|
125 |
HTML.encode(text) + "</pre></html>" |
|
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
126 |
|
| 40849 | 127 |
def tooltip_dismiss_delay(): Time = |
| 40852 | 128 |
Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
|
|
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 |
||
| 41382 | 150 |
/* check JVM */ |
151 |
||
152 |
def check_jvm() |
|
153 |
{
|
|
154 |
if (!Platform.is_hotspot) {
|
|
155 |
Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine", |
|
156 |
"This is " + Platform.jvm_name, |
|
157 |
"Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!") |
|
158 |
} |
|
159 |
} |
|
160 |
||
161 |
||
| 38221 | 162 |
/* 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
|
163 |
|
| 37177 | 164 |
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
|
165 |
|
| 37177 | 166 |
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
|
167 |
|
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
168 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
| 37177 | 169 |
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
|
170 |
|
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
171 |
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
|
172 |
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
|
173 |
|
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
174 |
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
|
175 |
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
|
176 |
|
| 38843 | 177 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
| 38640 | 178 |
{
|
179 |
try { buffer.readLock(); body }
|
|
180 |
finally { buffer.readUnlock() }
|
|
181 |
} |
|
182 |
||
| 38843 | 183 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
184 |
Swing_Thread.now { buffer_lock(buffer) { body } }
|
|
185 |
||
|
40474
576b88b1dce9
added buffer_text convenience, with explicit locking;
wenzelm
parents:
39741
diff
changeset
|
186 |
def buffer_text(buffer: JEditBuffer): String = |
|
576b88b1dce9
added buffer_text convenience, with explicit locking;
wenzelm
parents:
39741
diff
changeset
|
187 |
buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
|
|
576b88b1dce9
added buffer_text convenience, with explicit locking;
wenzelm
parents:
39741
diff
changeset
|
188 |
|
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
189 |
def buffer_path(buffer: Buffer): (String, String) = |
|
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
190 |
{
|
|
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
191 |
val master_dir = buffer.getDirectory |
|
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
192 |
val path = buffer.getSymlinkPath |
|
44225
a8f921e6484f
more robust Thy_Header.base_name, with minimal assumptions about path syntax;
wenzelm
parents:
44222
diff
changeset
|
193 |
(master_dir, path) |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
194 |
} |
|
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
195 |
|
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
196 |
|
| 43449 | 197 |
/* document model and view */ |
198 |
||
199 |
def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer) |
|
200 |
def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area) |
|
201 |
||
|
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
|
202 |
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
|
203 |
{
|
|
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
|
204 |
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
|
205 |
val 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
|
206 |
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
|
207 |
case Some(model) => Some(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
|
208 |
case None => |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
209 |
val (master_dir, path) = buffer_path(buffer) |
|
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
210 |
Thy_Header.thy_name(path) match {
|
|
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44221
diff
changeset
|
211 |
case Some(name) => |
|
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44221
diff
changeset
|
212 |
Some(Document_Model.init(session, buffer, master_dir, path, name)) |
|
44160
8848867501fb
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
wenzelm
parents:
43714
diff
changeset
|
213 |
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
|
214 |
} |
|
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 |
} |
|
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 |
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
|
217 |
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
|
218 |
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
|
219 |
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
|
220 |
} |
|
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
|
221 |
} |
|
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
|
222 |
} |
|
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
|
223 |
} |
|
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 |
|
|
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
|
225 |
def exit_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
|
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 |
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
|
228 |
jedit_text_areas(buffer).foreach(Document_View.exit) |
|
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 |
Document_Model.exit(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
|
230 |
} |
|
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 |
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
|
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 |
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
|
236 |
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
|
237 |
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
|
238 |
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
|
239 |
} |
|
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 |
} |
|
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 |
} |
|
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 |
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
|
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 |
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
|
246 |
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
|
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 |
} |
|
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 |
|
| 43449 | 250 |
|
| 37068 | 251 |
/* dockable windows */ |
252 |
||
253 |
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
254 |
||
| 39515 | 255 |
def docked_session(view: View): Option[Session_Dockable] = |
256 |
wm(view).getDockableWindow("isabelle-session") match {
|
|
257 |
case dockable: Session_Dockable => Some(dockable) |
|
258 |
case _ => None |
|
259 |
} |
|
260 |
||
| 37068 | 261 |
def docked_output(view: View): Option[Output_Dockable] = |
262 |
wm(view).getDockableWindow("isabelle-output") match {
|
|
263 |
case dockable: Output_Dockable => Some(dockable) |
|
264 |
case _ => None |
|
265 |
} |
|
266 |
||
267 |
def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
268 |
wm(view).getDockableWindow("isabelle-raw-output") match {
|
|
269 |
case dockable: Raw_Output_Dockable => Some(dockable) |
|
270 |
case _ => None |
|
271 |
} |
|
272 |
||
273 |
def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
274 |
wm(view).getDockableWindow("isabelle-protocol") match {
|
|
275 |
case dockable: Protocol_Dockable => Some(dockable) |
|
276 |
case _ => None |
|
277 |
} |
|
278 |
||
279 |
||
| 39517 | 280 |
/* logic image */ |
281 |
||
282 |
def default_logic(): String = |
|
283 |
{
|
|
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
284 |
val logic = Isabelle_System.getenv("JEDIT_LOGIC")
|
| 39517 | 285 |
if (logic != "") logic |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
286 |
else Isabelle_System.getenv_strict("ISABELLE_LOGIC")
|
| 39517 | 287 |
} |
288 |
||
289 |
class Logic_Entry(val name: String, val description: String) |
|
290 |
{
|
|
291 |
override def toString = description |
|
292 |
} |
|
293 |
||
294 |
def logic_selector(logic: String): ComboBox[Logic_Entry] = |
|
295 |
{
|
|
296 |
val entries = |
|
297 |
new Logic_Entry("", "default (" + default_logic() + ")") ::
|
|
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
298 |
Isabelle_System.find_logics().map(name => new Logic_Entry(name, name)) |
| 39517 | 299 |
val component = new ComboBox(entries) |
300 |
entries.find(_.name == logic) match {
|
|
301 |
case None => |
|
302 |
case Some(entry) => component.selection.item = entry |
|
303 |
} |
|
| 39702 | 304 |
component.tooltip = "Isabelle logic image" |
| 39517 | 305 |
component |
306 |
} |
|
| 39702 | 307 |
|
308 |
def start_session() |
|
309 |
{
|
|
| 40852 | 310 |
val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
|
|
43670
7f933761764b
prefer space_explode/split_lines as in Isabelle/ML;
wenzelm
parents:
43661
diff
changeset
|
311 |
val modes = space_explode(',', Isabelle_System.getenv("JEDIT_PRINT_MODE")).map("-m" + _)
|
| 39702 | 312 |
val logic = {
|
313 |
val logic = Property("logic")
|
|
314 |
if (logic != null && logic != "") logic |
|
315 |
else Isabelle.default_logic() |
|
316 |
} |
|
| 40850 | 317 |
session.start(timeout, modes ::: List(logic)) |
| 39702 | 318 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
319 |
} |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
320 |
|
| 34429 | 321 |
|
| 34618 | 322 |
class Plugin extends EBPlugin |
323 |
{
|
|
| 43645 | 324 |
/* editor file store */ |
325 |
||
326 |
private val file_store = new Session.File_Store |
|
327 |
{
|
|
| 44185 | 328 |
def append(master_dir: String, source_path: Path): String = |
| 43645 | 329 |
{
|
| 44185 | 330 |
val path = source_path.expand |
331 |
if (path.is_absolute) Isabelle_System.platform_path(path) |
|
332 |
else {
|
|
333 |
val vfs = VFSManager.getVFSForPath(master_dir) |
|
334 |
if (vfs.isInstanceOf[FileVFS]) |
|
|
44222
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44221
diff
changeset
|
335 |
MiscUtilities.resolveSymlinks( |
|
9d5ef6cd4ee1
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
wenzelm
parents:
44221
diff
changeset
|
336 |
vfs.constructPath(master_dir, Isabelle_System.platform_path(path))) |
| 44185 | 337 |
else vfs.constructPath(master_dir, Isabelle_System.standard_path(path)) |
338 |
} |
|
| 44163 | 339 |
} |
| 43645 | 340 |
|
| 44163 | 341 |
def require(canonical_name: String) |
342 |
{
|
|
343 |
Swing_Thread.later {
|
|
344 |
if (!Isabelle.jedit_buffers().exists(_.getSymlinkPath == canonical_name)) |
|
345 |
jEdit.openFile(null: View, canonical_name) |
|
| 43645 | 346 |
} |
347 |
} |
|
348 |
} |
|
349 |
||
350 |
||
351 |
/* session manager */ |
|
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
352 |
|
| 39633 | 353 |
private val session_manager = actor {
|
354 |
loop {
|
|
355 |
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
|
356 |
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
|
357 |
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
|
358 |
case Session.Failed => |
|
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
|
359 |
Swing_Thread.now {
|
|
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
|
360 |
val text = new scala.swing.TextArea(Isabelle.session.syslog()) |
|
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
|
361 |
text.editable = false |
|
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
|
362 |
Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) |
|
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
|
363 |
} |
|
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
|
364 |
|
|
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
|
365 |
case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_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
|
366 |
case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model) |
|
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
|
367 |
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
|
368 |
} |
|
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
|
369 |
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
|
370 |
} |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
371 |
} |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
372 |
} |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
373 |
|
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
374 |
|
| 34618 | 375 |
/* main plugin plumbing */ |
| 34433 | 376 |
|
| 34767 | 377 |
override def handleMessage(message: EBMessage) |
| 34618 | 378 |
{
|
|
43510
17d431c92575
init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;
wenzelm
parents:
43487
diff
changeset
|
379 |
Swing_Thread.assert() |
| 34767 | 380 |
message match {
|
|
41383
514bb82514df
check JVM later, to avoid potential conflict with jEdit splash screen;
wenzelm
parents:
41382
diff
changeset
|
381 |
case msg: EditorStarted => |
|
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
|
382 |
Isabelle.check_jvm() |
|
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
|
383 |
if (Isabelle.Boolean_Property("auto-start"))
|
|
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
|
384 |
Isabelle.start_session() |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
385 |
|
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37241
diff
changeset
|
386 |
case msg: BufferUpdate |
|
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
|
387 |
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => |
| 39634 | 388 |
|
| 39633 | 389 |
val buffer = msg.getBuffer |
| 43643 | 390 |
if (buffer != null && Isabelle.session.is_ready) |
|
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
|
391 |
Isabelle.init_model(buffer) |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37241
diff
changeset
|
392 |
|
| 39634 | 393 |
case msg: EditPaneUpdate |
|
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
|
394 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
|
39637
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
395 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
| 39634 | 396 |
msg.getWhat == EditPaneUpdate.CREATED || |
397 |
msg.getWhat == EditPaneUpdate.DESTROYED) => |
|
398 |
||
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
399 |
val edit_pane = msg.getEditPane |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
400 |
val buffer = edit_pane.getBuffer |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
401 |
val text_area = edit_pane.getTextArea |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
402 |
|
|
39637
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
403 |
if (buffer != null && text_area != null) {
|
|
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
|
404 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
|
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
|
405 |
msg.getWhat == EditPaneUpdate.CREATED) {
|
| 43643 | 406 |
if (Isabelle.session.is_ready) |
|
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
|
407 |
Isabelle.init_view(buffer, 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
|
408 |
} |
|
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
|
409 |
else Isabelle.exit_view(buffer, text_area) |
| 34671 | 410 |
} |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
411 |
|
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
412 |
case msg: PropertiesChanged => |
| 43390 | 413 |
Swing_Thread.now { Isabelle.setup_tooltips() }
|
| 34791 | 414 |
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
|
415 |
|
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
416 |
case _ => |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
417 |
} |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
418 |
} |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
419 |
|
| 34618 | 420 |
override def start() |
421 |
{
|
|
|
43443
5d9693c2337e
basic support for extended syntax styles: sub/superscript;
wenzelm
parents:
43390
diff
changeset
|
422 |
Isabelle.plugin = this |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
423 |
Isabelle.setup_tooltips() |
|
43661
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
424 |
Isabelle_System.init() |
|
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
425 |
Isabelle_System.install_fonts() |
|
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
426 |
Isabelle.session = new Session(file_store) |
|
39fdbd814c7f
quasi-static Isabelle_System -- reduced tendency towards "functorial style";
wenzelm
parents:
43648
diff
changeset
|
427 |
SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender) |
| 43513 | 428 |
if (ModeProvider.instance.isInstanceOf[ModeProvider]) |
429 |
ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance) |
|
| 39633 | 430 |
Isabelle.session.phase_changed += session_manager |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
431 |
} |
| 34618 | 432 |
|
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
433 |
override def stop() |
| 34618 | 434 |
{
|
| 43513 | 435 |
Isabelle.session.phase_changed -= session_manager |
436 |
Isabelle.jedit_buffers.foreach(Isabelle.exit_model) |
|
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
437 |
Isabelle.session.stop() |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
438 |
} |
|
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
439 |
} |