1 /* Title: Tools/jEdit/src/jedit/plugin.scala |
|
2 Author: Makarius |
|
3 |
|
4 Main Isabelle/jEdit plugin setup. |
|
5 */ |
|
6 |
|
7 package isabelle.jedit |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.io.{FileInputStream, IOException} |
|
13 import java.awt.Font |
|
14 |
|
15 import scala.collection.mutable |
|
16 import scala.swing.ComboBox |
|
17 |
|
18 import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin, |
|
19 Buffer, EditPane, ServiceManager, View} |
|
20 import org.gjt.sp.jedit.buffer.JEditBuffer |
|
21 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea} |
|
22 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged} |
|
23 import org.gjt.sp.jedit.gui.DockableWindowManager |
|
24 |
|
25 import org.gjt.sp.util.Log |
|
26 |
|
27 import scala.actors.Actor |
|
28 import Actor._ |
|
29 |
|
30 |
|
31 object Isabelle |
|
32 { |
|
33 /* plugin instance */ |
|
34 |
|
35 var system: Isabelle_System = null |
|
36 var session: Session = null |
|
37 |
|
38 |
|
39 /* properties */ |
|
40 |
|
41 val OPTION_PREFIX = "options.isabelle." |
|
42 |
|
43 object Property |
|
44 { |
|
45 def apply(name: String): String = |
|
46 jEdit.getProperty(OPTION_PREFIX + name) |
|
47 def apply(name: String, default: String): String = |
|
48 jEdit.getProperty(OPTION_PREFIX + name, default) |
|
49 def update(name: String, value: String) = |
|
50 jEdit.setProperty(OPTION_PREFIX + name, value) |
|
51 } |
|
52 |
|
53 object Boolean_Property |
|
54 { |
|
55 def apply(name: String): Boolean = |
|
56 jEdit.getBooleanProperty(OPTION_PREFIX + name) |
|
57 def apply(name: String, default: Boolean): Boolean = |
|
58 jEdit.getBooleanProperty(OPTION_PREFIX + name, default) |
|
59 def update(name: String, value: Boolean) = |
|
60 jEdit.setBooleanProperty(OPTION_PREFIX + name, value) |
|
61 } |
|
62 |
|
63 object Int_Property |
|
64 { |
|
65 def apply(name: String): Int = |
|
66 jEdit.getIntegerProperty(OPTION_PREFIX + name) |
|
67 def apply(name: String, default: Int): Int = |
|
68 jEdit.getIntegerProperty(OPTION_PREFIX + name, default) |
|
69 def update(name: String, value: Int) = |
|
70 jEdit.setIntegerProperty(OPTION_PREFIX + name, value) |
|
71 } |
|
72 |
|
73 object Double_Property |
|
74 { |
|
75 def apply(name: String): Double = |
|
76 jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0) |
|
77 def apply(name: String, default: Double): Double = |
|
78 jEdit.getDoubleProperty(OPTION_PREFIX + name, default) |
|
79 def update(name: String, value: Double) = |
|
80 jEdit.setDoubleProperty(OPTION_PREFIX + name, value) |
|
81 } |
|
82 |
|
83 object Time_Property |
|
84 { |
|
85 def apply(name: String): Time = |
|
86 Time.seconds(Double_Property(name)) |
|
87 def apply(name: String, default: Time): Time = |
|
88 Time.seconds(Double_Property(name, default.seconds)) |
|
89 def update(name: String, value: Time) = |
|
90 Double_Property.update(name, value.seconds) |
|
91 } |
|
92 |
|
93 |
|
94 /* font */ |
|
95 |
|
96 def font_family(): String = jEdit.getProperty("view.font") |
|
97 |
|
98 def font_size(): Float = |
|
99 (jEdit.getIntegerProperty("view.fontsize", 16) * |
|
100 Int_Property("relative-font-size", 100)).toFloat / 100 |
|
101 |
|
102 |
|
103 /* text area ranges */ |
|
104 |
|
105 case class Gfx_Range(val x: Int, val y: Int, val length: Int) |
|
106 |
|
107 def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] = |
|
108 { |
|
109 val p = text_area.offsetToXY(range.start) |
|
110 val q = text_area.offsetToXY(range.stop) |
|
111 if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x)) |
|
112 else None |
|
113 } |
|
114 |
|
115 |
|
116 /* tooltip markup */ |
|
117 |
|
118 def tooltip(text: String): String = |
|
119 "<html><pre style=\"font-family: " + font_family() + "; font-size: " + |
|
120 Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?) |
|
121 HTML.encode(text) + "</pre></html>" |
|
122 |
|
123 def tooltip_dismiss_delay(): Time = |
|
124 Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5) |
|
125 |
|
126 def setup_tooltips() |
|
127 { |
|
128 Swing_Thread.now { |
|
129 val manager = javax.swing.ToolTipManager.sharedInstance |
|
130 manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt) |
|
131 } |
|
132 } |
|
133 |
|
134 |
|
135 /* icons */ |
|
136 |
|
137 def load_icon(name: String): javax.swing.Icon = |
|
138 { |
|
139 val icon = GUIUtilities.loadIcon(name) |
|
140 if (icon.getIconWidth < 0 || icon.getIconHeight < 0) |
|
141 Log.log(Log.ERROR, icon, "Bad icon: " + name) |
|
142 icon |
|
143 } |
|
144 |
|
145 |
|
146 /* check JVM */ |
|
147 |
|
148 def check_jvm() |
|
149 { |
|
150 if (!Platform.is_hotspot) { |
|
151 Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine", |
|
152 "This is " + Platform.jvm_name, |
|
153 "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!") |
|
154 } |
|
155 } |
|
156 |
|
157 |
|
158 /* main jEdit components */ |
|
159 |
|
160 def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator |
|
161 |
|
162 def jedit_views(): Iterator[View] = jEdit.getViews().iterator |
|
163 |
|
164 def jedit_text_areas(view: View): Iterator[JEditTextArea] = |
|
165 view.getEditPanes().iterator.map(_.getTextArea) |
|
166 |
|
167 def jedit_text_areas(): Iterator[JEditTextArea] = |
|
168 jedit_views().flatMap(jedit_text_areas(_)) |
|
169 |
|
170 def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] = |
|
171 jedit_text_areas().filter(_.getBuffer == buffer) |
|
172 |
|
173 def buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
174 { |
|
175 try { buffer.readLock(); body } |
|
176 finally { buffer.readUnlock() } |
|
177 } |
|
178 |
|
179 def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A = |
|
180 Swing_Thread.now { buffer_lock(buffer) { body } } |
|
181 |
|
182 def buffer_text(buffer: JEditBuffer): String = |
|
183 buffer_lock(buffer) { buffer.getText(0, buffer.getLength) } |
|
184 |
|
185 |
|
186 /* dockable windows */ |
|
187 |
|
188 private def wm(view: View): DockableWindowManager = view.getDockableWindowManager |
|
189 |
|
190 def docked_session(view: View): Option[Session_Dockable] = |
|
191 wm(view).getDockableWindow("isabelle-session") match { |
|
192 case dockable: Session_Dockable => Some(dockable) |
|
193 case _ => None |
|
194 } |
|
195 |
|
196 def docked_output(view: View): Option[Output_Dockable] = |
|
197 wm(view).getDockableWindow("isabelle-output") match { |
|
198 case dockable: Output_Dockable => Some(dockable) |
|
199 case _ => None |
|
200 } |
|
201 |
|
202 def docked_raw_output(view: View): Option[Raw_Output_Dockable] = |
|
203 wm(view).getDockableWindow("isabelle-raw-output") match { |
|
204 case dockable: Raw_Output_Dockable => Some(dockable) |
|
205 case _ => None |
|
206 } |
|
207 |
|
208 def docked_protocol(view: View): Option[Protocol_Dockable] = |
|
209 wm(view).getDockableWindow("isabelle-protocol") match { |
|
210 case dockable: Protocol_Dockable => Some(dockable) |
|
211 case _ => None |
|
212 } |
|
213 |
|
214 |
|
215 /* logic image */ |
|
216 |
|
217 def default_logic(): String = |
|
218 { |
|
219 val logic = system.getenv("JEDIT_LOGIC") |
|
220 if (logic != "") logic |
|
221 else system.getenv_strict("ISABELLE_LOGIC") |
|
222 } |
|
223 |
|
224 class Logic_Entry(val name: String, val description: String) |
|
225 { |
|
226 override def toString = description |
|
227 } |
|
228 |
|
229 def logic_selector(logic: String): ComboBox[Logic_Entry] = |
|
230 { |
|
231 val entries = |
|
232 new Logic_Entry("", "default (" + default_logic() + ")") :: |
|
233 system.find_logics().map(name => new Logic_Entry(name, name)) |
|
234 val component = new ComboBox(entries) |
|
235 entries.find(_.name == logic) match { |
|
236 case None => |
|
237 case Some(entry) => component.selection.item = entry |
|
238 } |
|
239 component.tooltip = "Isabelle logic image" |
|
240 component |
|
241 } |
|
242 |
|
243 def start_session() |
|
244 { |
|
245 val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5) |
|
246 val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _) |
|
247 val logic = { |
|
248 val logic = Property("logic") |
|
249 if (logic != null && logic != "") logic |
|
250 else Isabelle.default_logic() |
|
251 } |
|
252 session.start(timeout, modes ::: List(logic)) |
|
253 } |
|
254 } |
|
255 |
|
256 |
|
257 class Plugin extends EBPlugin |
|
258 { |
|
259 /* session management */ |
|
260 |
|
261 private def init_model(buffer: Buffer) |
|
262 { |
|
263 Isabelle.swing_buffer_lock(buffer) { |
|
264 val opt_model = |
|
265 Document_Model(buffer) match { |
|
266 case Some(model) => model.refresh; Some(model) |
|
267 case None => |
|
268 Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match { |
|
269 case Some((dir, thy_name)) => |
|
270 Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name)) |
|
271 case None => None |
|
272 } |
|
273 } |
|
274 if (opt_model.isDefined) { |
|
275 for (text_area <- Isabelle.jedit_text_areas(buffer)) { |
|
276 if (Document_View(text_area).map(_.model) != opt_model) |
|
277 Document_View.init(opt_model.get, text_area) |
|
278 } |
|
279 } |
|
280 } |
|
281 } |
|
282 |
|
283 private def exit_model(buffer: Buffer) |
|
284 { |
|
285 Isabelle.swing_buffer_lock(buffer) { |
|
286 Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit) |
|
287 Document_Model.exit(buffer) |
|
288 } |
|
289 } |
|
290 |
|
291 private case class Init_Model(buffer: Buffer) |
|
292 private case class Exit_Model(buffer: Buffer) |
|
293 private case class Init_View(buffer: Buffer, text_area: JEditTextArea) |
|
294 private case class Exit_View(buffer: Buffer, text_area: JEditTextArea) |
|
295 |
|
296 private val session_manager = actor { |
|
297 var ready = false |
|
298 loop { |
|
299 react { |
|
300 case phase: Session.Phase => |
|
301 ready = phase == Session.Ready |
|
302 phase match { |
|
303 case Session.Failed => |
|
304 Swing_Thread.now { |
|
305 val text = new scala.swing.TextArea(Isabelle.session.syslog()) |
|
306 text.editable = false |
|
307 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text) |
|
308 } |
|
309 |
|
310 case Session.Ready => Isabelle.jedit_buffers.foreach(init_model) |
|
311 case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model) |
|
312 case _ => |
|
313 } |
|
314 |
|
315 case Init_Model(buffer) => |
|
316 if (ready) init_model(buffer) |
|
317 |
|
318 case Exit_Model(buffer) => |
|
319 exit_model(buffer) |
|
320 |
|
321 case Init_View(buffer, text_area) => |
|
322 if (ready) { |
|
323 Isabelle.swing_buffer_lock(buffer) { |
|
324 Document_Model(buffer) match { |
|
325 case Some(model) => Document_View.init(model, text_area) |
|
326 case None => |
|
327 } |
|
328 } |
|
329 } |
|
330 |
|
331 case Exit_View(buffer, text_area) => |
|
332 Isabelle.swing_buffer_lock(buffer) { |
|
333 Document_View.exit(text_area) |
|
334 } |
|
335 |
|
336 case bad => System.err.println("session_manager: ignoring bad message " + bad) |
|
337 } |
|
338 } |
|
339 } |
|
340 |
|
341 |
|
342 /* main plugin plumbing */ |
|
343 |
|
344 override def handleMessage(message: EBMessage) |
|
345 { |
|
346 message match { |
|
347 case msg: EditorStarted => |
|
348 Isabelle.check_jvm() |
|
349 if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session() |
|
350 |
|
351 case msg: BufferUpdate |
|
352 if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED => |
|
353 |
|
354 val buffer = msg.getBuffer |
|
355 if (buffer != null) session_manager ! Init_Model(buffer) |
|
356 |
|
357 case msg: EditPaneUpdate |
|
358 if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING || |
|
359 msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
|
360 msg.getWhat == EditPaneUpdate.CREATED || |
|
361 msg.getWhat == EditPaneUpdate.DESTROYED) => |
|
362 |
|
363 val edit_pane = msg.getEditPane |
|
364 val buffer = edit_pane.getBuffer |
|
365 val text_area = edit_pane.getTextArea |
|
366 |
|
367 if (buffer != null && text_area != null) { |
|
368 if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED || |
|
369 msg.getWhat == EditPaneUpdate.CREATED) |
|
370 session_manager ! Init_View(buffer, text_area) |
|
371 else |
|
372 session_manager ! Exit_View(buffer, text_area) |
|
373 } |
|
374 |
|
375 case msg: PropertiesChanged => |
|
376 Swing_Thread.now { |
|
377 Isabelle.setup_tooltips() |
|
378 for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined) |
|
379 Document_View(text_area).get.extend_styles() |
|
380 } |
|
381 Isabelle.session.global_settings.event(Session.Global_Settings) |
|
382 |
|
383 case _ => |
|
384 } |
|
385 } |
|
386 |
|
387 override def start() |
|
388 { |
|
389 Isabelle.setup_tooltips() |
|
390 Isabelle.system = new Isabelle_System |
|
391 Isabelle.system.install_fonts() |
|
392 Isabelle.session = new Session(Isabelle.system) |
|
393 Isabelle.session.phase_changed += session_manager |
|
394 } |
|
395 |
|
396 override def stop() |
|
397 { |
|
398 Isabelle.session.stop() |
|
399 Isabelle.session.phase_changed -= session_manager |
|
400 } |
|
401 } |
|