author | wenzelm |
Tue, 28 Sep 2010 15:58:31 +0200 | |
changeset 39735 | 969ede84aac0 |
parent 39702 | d7c256cb2797 |
child 39741 | 62b91eb2d39a |
permissions | -rw-r--r-- |
36760 | 1 |
/* Title: Tools/jEdit/src/jedit/plugin.scala |
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 |
||
34429 | 12 |
import java.io.{FileInputStream, IOException} |
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
13 |
import java.awt.Font |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
14 |
|
34497 | 15 |
import scala.collection.mutable |
39517 | 16 |
import scala.swing.ComboBox |
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
17 |
|
39241 | 18 |
import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, |
19 |
Buffer, EditPane, ServiceManager, View} |
|
34406
f81cd75ae331
restructured: independent provers in different buffers
immler@in.tum.de
parents:
34337
diff
changeset
|
20 |
import org.gjt.sp.jedit.buffer.JEditBuffer |
39043 | 21 |
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
39633 | 22 |
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} |
37068 | 23 |
import org.gjt.sp.jedit.gui.DockableWindowManager |
34429 | 24 |
|
39241 | 25 |
import org.gjt.sp.util.Log |
26 |
||
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
27 |
import scala.actors.Actor |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
28 |
import Actor._ |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
29 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
30 |
|
34618 | 31 |
object Isabelle |
32 |
{ |
|
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
33 |
/* plugin instance */ |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
34 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
35 |
var system: Isabelle_System = null |
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
36 |
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
|
37 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
38 |
|
34618 | 39 |
/* properties */ |
40 |
||
41 |
val OPTION_PREFIX = "options.isabelle." |
|
42 |
||
43 |
object Property |
|
44 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
45 |
def apply(name: String): String = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
46 |
jEdit.getProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
47 |
def apply(name: String, default: String): String = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
48 |
jEdit.getProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
49 |
def update(name: String, value: String) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
50 |
jEdit.setProperty(OPTION_PREFIX + name, value) |
34468
9d4b4f290676
maintain Isabelle properties via object Isabelle.Property with apply/update methods;
wenzelm
parents:
34463
diff
changeset
|
51 |
} |
34433 | 52 |
|
34618 | 53 |
object Boolean_Property |
54 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
55 |
def apply(name: String): Boolean = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
56 |
jEdit.getBooleanProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
57 |
def apply(name: String, default: Boolean): Boolean = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
58 |
jEdit.getBooleanProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
59 |
def update(name: String, value: Boolean) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
60 |
jEdit.setBooleanProperty(OPTION_PREFIX + name, value) |
34618 | 61 |
} |
62 |
||
63 |
object Int_Property |
|
64 |
{ |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
65 |
def apply(name: String): Int = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
66 |
jEdit.getIntegerProperty(OPTION_PREFIX + name) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
67 |
def apply(name: String, default: Int): Int = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
68 |
jEdit.getIntegerProperty(OPTION_PREFIX + name, default) |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
69 |
def update(name: String, value: Int) = |
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
70 |
jEdit.setIntegerProperty(OPTION_PREFIX + name, value) |
34618 | 71 |
} |
72 |
||
37164 | 73 |
|
74 |
/* font */ |
|
75 |
||
76 |
def font_family(): String = jEdit.getProperty("view.font") |
|
77 |
||
37019 | 78 |
def font_size(): Float = |
79 |
(jEdit.getIntegerProperty("view.fontsize", 16) * |
|
80 |
Int_Property("relative-font-size", 100)).toFloat / 100 |
|
36814
dc85664dbf6d
support Isabelle plugin properties with defaults;
wenzelm
parents:
36760
diff
changeset
|
81 |
|
34618 | 82 |
|
39043 | 83 |
/* text area ranges */ |
84 |
||
85 |
case class Gfx_Range(val x: Int, val y: Int, val length: Int) |
|
86 |
||
87 |
def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
88 |
{ |
|
89 |
val p = text_area.offsetToXY(range.start) |
|
90 |
val q = text_area.offsetToXY(range.stop) |
|
91 |
if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) |
|
92 |
else None |
|
93 |
} |
|
94 |
||
95 |
||
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
96 |
/* tooltip markup */ |
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
97 |
|
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
98 |
def tooltip(text: String): String = |
37203
c4261f3bbdd7
more flexibile font size via CSS <style> instead of old <font> element;
wenzelm
parents:
37201
diff
changeset
|
99 |
"<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
|
100 |
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
|
101 |
HTML.encode(text) + "</pre></html>" |
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
102 |
|
38854
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
103 |
def tooltip_dismiss_delay(): Int = |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
104 |
Int_Property("tooltip-dismiss-delay", 8000) max 500 |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
105 |
|
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
106 |
def setup_tooltips() |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
107 |
{ |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
108 |
Swing_Thread.now { |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
109 |
val manager = javax.swing.ToolTipManager.sharedInstance |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
110 |
manager.setDismissDelay(tooltip_dismiss_delay()) |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
111 |
} |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
112 |
} |
eb6a35be18ca
Isabelle/jEdit property for global tooltip dismiss delay;
wenzelm
parents:
38843
diff
changeset
|
113 |
|
37201
8517a650cfdc
control tooltip font via Swing HTML, with tooltip-font-size property;
wenzelm
parents:
37177
diff
changeset
|
114 |
|
39241 | 115 |
/* icons */ |
116 |
||
117 |
def load_icon(name: String): javax.swing.Icon = |
|
118 |
{ |
|
119 |
val icon = GUIUtilities.loadIcon(name) |
|
120 |
if (icon.getIconWidth < 0 || icon.getIconHeight < 0) |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
121 |
Log.log(Log.ERROR, icon, "Bad icon: " + name) |
39241 | 122 |
icon |
123 |
} |
|
124 |
||
125 |
||
38221 | 126 |
/* 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
|
127 |
|
37177 | 128 |
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
|
129 |
|
37177 | 130 |
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
|
131 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
132 |
def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
37177 | 133 |
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
|
134 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
135 |
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
|
136 |
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
|
137 |
|
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
138 |
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
|
139 |
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
|
140 |
|
38843 | 141 |
def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
38640 | 142 |
{ |
143 |
try { buffer.readLock(); body } |
|
144 |
finally { buffer.readUnlock() } |
|
145 |
} |
|
146 |
||
38843 | 147 |
def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
148 |
Swing_Thread.now { buffer_lock(buffer) { body } } |
|
149 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
150 |
|
37068 | 151 |
/* dockable windows */ |
152 |
||
153 |
private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
154 |
||
39515 | 155 |
def docked_session(view: View): Option[Session_Dockable] = |
156 |
wm(view).getDockableWindow("isabelle-session") match { |
|
157 |
case dockable: Session_Dockable => Some(dockable) |
|
158 |
case _ => None |
|
159 |
} |
|
160 |
||
37068 | 161 |
def docked_output(view: View): Option[Output_Dockable] = |
162 |
wm(view).getDockableWindow("isabelle-output") match { |
|
163 |
case dockable: Output_Dockable => Some(dockable) |
|
164 |
case _ => None |
|
165 |
} |
|
166 |
||
167 |
def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
168 |
wm(view).getDockableWindow("isabelle-raw-output") match { |
|
169 |
case dockable: Raw_Output_Dockable => Some(dockable) |
|
170 |
case _ => None |
|
171 |
} |
|
172 |
||
173 |
def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
174 |
wm(view).getDockableWindow("isabelle-protocol") match { |
|
175 |
case dockable: Protocol_Dockable => Some(dockable) |
|
176 |
case _ => None |
|
177 |
} |
|
178 |
||
179 |
||
39517 | 180 |
/* logic image */ |
181 |
||
182 |
def default_logic(): String = |
|
183 |
{ |
|
184 |
val logic = system.getenv("JEDIT_LOGIC") |
|
185 |
if (logic != "") logic |
|
186 |
else system.getenv_strict("ISABELLE_LOGIC") |
|
187 |
} |
|
188 |
||
189 |
class Logic_Entry(val name: String, val description: String) |
|
190 |
{ |
|
191 |
override def toString = description |
|
192 |
} |
|
193 |
||
194 |
def logic_selector(logic: String): ComboBox[Logic_Entry] = |
|
195 |
{ |
|
196 |
val entries = |
|
197 |
new Logic_Entry("", "default (" + default_logic() + ")") :: |
|
198 |
system.find_logics().map(name => new Logic_Entry(name, name)) |
|
199 |
val component = new ComboBox(entries) |
|
200 |
entries.find(_.name == logic) match { |
|
201 |
case None => |
|
202 |
case Some(entry) => component.selection.item = entry |
|
203 |
} |
|
39702 | 204 |
component.tooltip = "Isabelle logic image" |
39517 | 205 |
component |
206 |
} |
|
39702 | 207 |
|
208 |
def start_session() |
|
209 |
{ |
|
210 |
val timeout = Int_Property("startup-timeout") max 1000 |
|
211 |
val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) |
|
212 |
val logic = { |
|
213 |
val logic = Property("logic") |
|
214 |
if (logic != null && logic != "") logic |
|
215 |
else Isabelle.default_logic() |
|
216 |
} |
|
217 |
session.start(timeout, modes ::: List(logic)) |
|
218 |
} |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
219 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
220 |
|
34429 | 221 |
|
34618 | 222 |
class Plugin extends EBPlugin |
223 |
{ |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
224 |
/* session management */ |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
225 |
|
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
|
226 |
private def init_model(buffer: Buffer) |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
227 |
{ |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
228 |
Isabelle.swing_buffer_lock(buffer) { |
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
|
229 |
val opt_model = |
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
|
230 |
Document_Model(buffer) 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
|
231 |
case Some(model) => model.refresh; Some(model) |
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
|
232 |
case None => |
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
|
233 |
Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) 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
|
234 |
case Some((_, thy_name)) => |
969ede84aac0
more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;
wenzelm
parents:
39702
diff
changeset
|
235 |
Some(Document_Model.init(Isabelle.session, buffer, thy_name)) |
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
|
236 |
case None => None |
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
|
237 |
} |
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
|
238 |
} |
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
|
239 |
if (opt_model.isDefined) { |
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
|
240 |
for (text_area <- Isabelle.jedit_text_areas(buffer)) { |
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
|
241 |
if (Document_View(text_area).map(_.model) != opt_model) |
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
|
242 |
Document_View.init(opt_model.get, text_area) |
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
|
243 |
} |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
244 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
245 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
246 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
247 |
|
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
|
248 |
private def exit_model(buffer: Buffer) |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
249 |
{ |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
250 |
Isabelle.swing_buffer_lock(buffer) { |
39637
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
251 |
Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) |
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
252 |
Document_Model.exit(buffer) |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
253 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
254 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
255 |
|
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
|
256 |
private case class Init_Model(buffer: Buffer) |
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
|
257 |
private case class Exit_Model(buffer: Buffer) |
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
|
258 |
private case class Init_View(buffer: Buffer, text_area: TextArea) |
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
|
259 |
private case class Exit_View(buffer: Buffer, text_area: TextArea) |
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
|
260 |
|
39633 | 261 |
private val session_manager = actor { |
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
|
262 |
var ready = false |
39633 | 263 |
loop { |
264 |
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
|
265 |
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
|
266 |
ready = phase == Session.Ready |
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
|
267 |
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
|
268 |
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
|
269 |
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
|
270 |
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
|
271 |
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
|
272 |
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
|
273 |
} |
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
|
274 |
|
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
|
275 |
case Session.Ready => Isabelle.jedit_buffers.foreach(init_model) |
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
|
276 |
case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model) |
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
|
277 |
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
|
278 |
} |
969ede84aac0
more uniform init/exit model/view in session_manager, trading race wrt. session.phase for race wrt. global editor state;
wenzelm
parents:
39702
diff
changeset
|
279 |
|
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
|
280 |
case Init_Model(buffer) => |
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
|
281 |
if (ready) init_model(buffer) |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
282 |
|
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
|
283 |
case Exit_Model(buffer) => |
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
|
284 |
exit_model(buffer) |
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
|
285 |
|
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
|
286 |
case Init_View(buffer, text_area) => |
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
|
287 |
if (ready) { |
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
|
288 |
Isabelle.swing_buffer_lock(buffer) { |
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
|
289 |
Document_Model(buffer) 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
|
290 |
case Some(model) => Document_View.init(model, text_area) |
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
|
291 |
case None => |
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
|
292 |
} |
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
|
293 |
} |
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
|
294 |
} |
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
|
295 |
|
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
|
296 |
case Exit_View(buffer, text_area) => |
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
|
297 |
Isabelle.swing_buffer_lock(buffer) { |
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
|
298 |
Document_View.exit(text_area) |
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
|
299 |
} |
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
|
300 |
|
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
|
301 |
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
|
302 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
303 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
304 |
} |
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
305 |
|
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
306 |
|
34618 | 307 |
/* main plugin plumbing */ |
34433 | 308 |
|
34767 | 309 |
override def handleMessage(message: EBMessage) |
34618 | 310 |
{ |
34767 | 311 |
message match { |
39702 | 312 |
case msg: EditorStarted |
313 |
if Isabelle.Boolean_Property("auto-start") => Isabelle.start_session() |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
314 |
|
37557
1ae272fd4082
refresh Isabelle token marker after buffer properties changed, e.g. when fold mode is switched;
wenzelm
parents:
37241
diff
changeset
|
315 |
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
|
316 |
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => |
39634 | 317 |
|
39633 | 318 |
val buffer = msg.getBuffer |
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
|
319 |
if (buffer != null) session_manager ! 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
|
320 |
|
39634 | 321 |
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
|
322 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
39637
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
323 |
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
39634 | 324 |
msg.getWhat == EditPaneUpdate.CREATED || |
325 |
msg.getWhat == EditPaneUpdate.DESTROYED) => |
|
326 |
||
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
327 |
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
|
328 |
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
|
329 |
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
|
330 |
|
39637
cc3452317b5f
slightly more robust EditBus plumbing wrt. Document_View/Document_Model;
wenzelm
parents:
39634
diff
changeset
|
331 |
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
|
332 |
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
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
|
333 |
msg.getWhat == EditPaneUpdate.CREATED) |
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
|
334 |
session_manager ! Init_View(buffer, text_area) |
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
|
335 |
else |
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
|
336 |
session_manager ! Exit_View(buffer, text_area) |
34671 | 337 |
} |
34784
02959dcea756
split Theory_View into Document_Model (connected to Buffer) and Document_View (connected to JEditTextArea);
wenzelm
parents:
34782
diff
changeset
|
338 |
|
34777
91d6089cef88
class Session models full session, with or without prover process (cf. heaps, browser_info);
wenzelm
parents:
34774
diff
changeset
|
339 |
case msg: PropertiesChanged => |
37241
04d2521e79b0
basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
wenzelm
parents:
37203
diff
changeset
|
340 |
Swing_Thread.now { |
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
341 |
Isabelle.setup_tooltips() |
37241
04d2521e79b0
basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
wenzelm
parents:
37203
diff
changeset
|
342 |
for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) |
04d2521e79b0
basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
wenzelm
parents:
37203
diff
changeset
|
343 |
Document_View(text_area).get.extend_styles() |
04d2521e79b0
basic support for sub/superscript token markup -- NB: need to maintain extended token types eagerly, since jEdit occasionally reinstalls a style array that is too short;
wenzelm
parents:
37203
diff
changeset
|
344 |
} |
34791 | 345 |
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
|
346 |
|
34318
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
347 |
case _ => |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
348 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
349 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
350 |
|
34618 | 351 |
override def start() |
352 |
{ |
|
39630
44181423183a
explicit Session.Phase indication with associated event bus;
wenzelm
parents:
39628
diff
changeset
|
353 |
Isabelle.setup_tooltips() |
34615 | 354 |
Isabelle.system = new Isabelle_System |
34774 | 355 |
Isabelle.system.install_fonts() |
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
356 |
Isabelle.session = new Session(Isabelle.system) |
39633 | 357 |
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
|
358 |
} |
34618 | 359 |
|
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
360 |
override def stop() |
34618 | 361 |
{ |
39628
f6e82967b5cd
Plugin.stop: refrain from invalidating Isabelle.session -- some actors/dockables out there might still refer to it;
wenzelm
parents:
39518
diff
changeset
|
362 |
Isabelle.session.stop() |
39633 | 363 |
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
|
364 |
} |
c13e168a8ae6
original sources from Johannes Hölzl a48e0c6ab1aea77c52d596f7efc007a543d3d10c with minor modifications of directory layout;
wenzelm
parents:
diff
changeset
|
365 |
} |