1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Jun 08 17:01:07 2011 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,401 +0,0 @@
1.4 -/* Title: Tools/jEdit/src/jedit/plugin.scala
1.5 - Author: Makarius
1.6 -
1.7 -Main Isabelle/jEdit plugin setup.
1.8 -*/
1.9 -
1.10 -package isabelle.jedit
1.11 -
1.12 -
1.13 -import isabelle._
1.14 -
1.15 -import java.io.{FileInputStream, IOException}
1.16 -import java.awt.Font
1.17 -
1.18 -import scala.collection.mutable
1.19 -import scala.swing.ComboBox
1.20 -
1.21 -import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
1.22 - Buffer, EditPane, ServiceManager, View}
1.23 -import org.gjt.sp.jedit.buffer.JEditBuffer
1.24 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
1.25 -import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
1.26 -import org.gjt.sp.jedit.gui.DockableWindowManager
1.27 -
1.28 -import org.gjt.sp.util.Log
1.29 -
1.30 -import scala.actors.Actor
1.31 -import Actor._
1.32 -
1.33 -
1.34 -object Isabelle
1.35 -{
1.36 - /* plugin instance */
1.37 -
1.38 - var system: Isabelle_System = null
1.39 - var session: Session = null
1.40 -
1.41 -
1.42 - /* properties */
1.43 -
1.44 - val OPTION_PREFIX = "options.isabelle."
1.45 -
1.46 - object Property
1.47 - {
1.48 - def apply(name: String): String =
1.49 - jEdit.getProperty(OPTION_PREFIX + name)
1.50 - def apply(name: String, default: String): String =
1.51 - jEdit.getProperty(OPTION_PREFIX + name, default)
1.52 - def update(name: String, value: String) =
1.53 - jEdit.setProperty(OPTION_PREFIX + name, value)
1.54 - }
1.55 -
1.56 - object Boolean_Property
1.57 - {
1.58 - def apply(name: String): Boolean =
1.59 - jEdit.getBooleanProperty(OPTION_PREFIX + name)
1.60 - def apply(name: String, default: Boolean): Boolean =
1.61 - jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
1.62 - def update(name: String, value: Boolean) =
1.63 - jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
1.64 - }
1.65 -
1.66 - object Int_Property
1.67 - {
1.68 - def apply(name: String): Int =
1.69 - jEdit.getIntegerProperty(OPTION_PREFIX + name)
1.70 - def apply(name: String, default: Int): Int =
1.71 - jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
1.72 - def update(name: String, value: Int) =
1.73 - jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
1.74 - }
1.75 -
1.76 - object Double_Property
1.77 - {
1.78 - def apply(name: String): Double =
1.79 - jEdit.getDoubleProperty(OPTION_PREFIX + name, 0.0)
1.80 - def apply(name: String, default: Double): Double =
1.81 - jEdit.getDoubleProperty(OPTION_PREFIX + name, default)
1.82 - def update(name: String, value: Double) =
1.83 - jEdit.setDoubleProperty(OPTION_PREFIX + name, value)
1.84 - }
1.85 -
1.86 - object Time_Property
1.87 - {
1.88 - def apply(name: String): Time =
1.89 - Time.seconds(Double_Property(name))
1.90 - def apply(name: String, default: Time): Time =
1.91 - Time.seconds(Double_Property(name, default.seconds))
1.92 - def update(name: String, value: Time) =
1.93 - Double_Property.update(name, value.seconds)
1.94 - }
1.95 -
1.96 -
1.97 - /* font */
1.98 -
1.99 - def font_family(): String = jEdit.getProperty("view.font")
1.100 -
1.101 - def font_size(): Float =
1.102 - (jEdit.getIntegerProperty("view.fontsize", 16) *
1.103 - Int_Property("relative-font-size", 100)).toFloat / 100
1.104 -
1.105 -
1.106 - /* text area ranges */
1.107 -
1.108 - case class Gfx_Range(val x: Int, val y: Int, val length: Int)
1.109 -
1.110 - def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
1.111 - {
1.112 - val p = text_area.offsetToXY(range.start)
1.113 - val q = text_area.offsetToXY(range.stop)
1.114 - if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
1.115 - else None
1.116 - }
1.117 -
1.118 -
1.119 - /* tooltip markup */
1.120 -
1.121 - def tooltip(text: String): String =
1.122 - "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
1.123 - Int_Property("tooltip-font-size", 10).toString + "px; \">" + // FIXME proper scaling (!?)
1.124 - HTML.encode(text) + "</pre></html>"
1.125 -
1.126 - def tooltip_dismiss_delay(): Time =
1.127 - Time_Property("tooltip-dismiss-delay", Time.seconds(8.0)) max Time.seconds(0.5)
1.128 -
1.129 - def setup_tooltips()
1.130 - {
1.131 - Swing_Thread.now {
1.132 - val manager = javax.swing.ToolTipManager.sharedInstance
1.133 - manager.setDismissDelay(tooltip_dismiss_delay().ms.toInt)
1.134 - }
1.135 - }
1.136 -
1.137 -
1.138 - /* icons */
1.139 -
1.140 - def load_icon(name: String): javax.swing.Icon =
1.141 - {
1.142 - val icon = GUIUtilities.loadIcon(name)
1.143 - if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
1.144 - Log.log(Log.ERROR, icon, "Bad icon: " + name)
1.145 - icon
1.146 - }
1.147 -
1.148 -
1.149 - /* check JVM */
1.150 -
1.151 - def check_jvm()
1.152 - {
1.153 - if (!Platform.is_hotspot) {
1.154 - Library.warning_dialog(jEdit.getActiveView, "Bad Java Virtual Machine",
1.155 - "This is " + Platform.jvm_name,
1.156 - "Isabelle/jEdit requires Java Hotspot from Sun/Oracle/Apple!")
1.157 - }
1.158 - }
1.159 -
1.160 -
1.161 - /* main jEdit components */
1.162 -
1.163 - def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
1.164 -
1.165 - def jedit_views(): Iterator[View] = jEdit.getViews().iterator
1.166 -
1.167 - def jedit_text_areas(view: View): Iterator[JEditTextArea] =
1.168 - view.getEditPanes().iterator.map(_.getTextArea)
1.169 -
1.170 - def jedit_text_areas(): Iterator[JEditTextArea] =
1.171 - jedit_views().flatMap(jedit_text_areas(_))
1.172 -
1.173 - def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
1.174 - jedit_text_areas().filter(_.getBuffer == buffer)
1.175 -
1.176 - def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
1.177 - {
1.178 - try { buffer.readLock(); body }
1.179 - finally { buffer.readUnlock() }
1.180 - }
1.181 -
1.182 - def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
1.183 - Swing_Thread.now { buffer_lock(buffer) { body } }
1.184 -
1.185 - def buffer_text(buffer: JEditBuffer): String =
1.186 - buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
1.187 -
1.188 -
1.189 - /* dockable windows */
1.190 -
1.191 - private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
1.192 -
1.193 - def docked_session(view: View): Option[Session_Dockable] =
1.194 - wm(view).getDockableWindow("isabelle-session") match {
1.195 - case dockable: Session_Dockable => Some(dockable)
1.196 - case _ => None
1.197 - }
1.198 -
1.199 - def docked_output(view: View): Option[Output_Dockable] =
1.200 - wm(view).getDockableWindow("isabelle-output") match {
1.201 - case dockable: Output_Dockable => Some(dockable)
1.202 - case _ => None
1.203 - }
1.204 -
1.205 - def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
1.206 - wm(view).getDockableWindow("isabelle-raw-output") match {
1.207 - case dockable: Raw_Output_Dockable => Some(dockable)
1.208 - case _ => None
1.209 - }
1.210 -
1.211 - def docked_protocol(view: View): Option[Protocol_Dockable] =
1.212 - wm(view).getDockableWindow("isabelle-protocol") match {
1.213 - case dockable: Protocol_Dockable => Some(dockable)
1.214 - case _ => None
1.215 - }
1.216 -
1.217 -
1.218 - /* logic image */
1.219 -
1.220 - def default_logic(): String =
1.221 - {
1.222 - val logic = system.getenv("JEDIT_LOGIC")
1.223 - if (logic != "") logic
1.224 - else system.getenv_strict("ISABELLE_LOGIC")
1.225 - }
1.226 -
1.227 - class Logic_Entry(val name: String, val description: String)
1.228 - {
1.229 - override def toString = description
1.230 - }
1.231 -
1.232 - def logic_selector(logic: String): ComboBox[Logic_Entry] =
1.233 - {
1.234 - val entries =
1.235 - new Logic_Entry("", "default (" + default_logic() + ")") ::
1.236 - system.find_logics().map(name => new Logic_Entry(name, name))
1.237 - val component = new ComboBox(entries)
1.238 - entries.find(_.name == logic) match {
1.239 - case None =>
1.240 - case Some(entry) => component.selection.item = entry
1.241 - }
1.242 - component.tooltip = "Isabelle logic image"
1.243 - component
1.244 - }
1.245 -
1.246 - def start_session()
1.247 - {
1.248 - val timeout = Time_Property("startup-timeout", Time.seconds(10)) max Time.seconds(5)
1.249 - val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
1.250 - val logic = {
1.251 - val logic = Property("logic")
1.252 - if (logic != null && logic != "") logic
1.253 - else Isabelle.default_logic()
1.254 - }
1.255 - session.start(timeout, modes ::: List(logic))
1.256 - }
1.257 -}
1.258 -
1.259 -
1.260 -class Plugin extends EBPlugin
1.261 -{
1.262 - /* session management */
1.263 -
1.264 - private def init_model(buffer: Buffer)
1.265 - {
1.266 - Isabelle.swing_buffer_lock(buffer) {
1.267 - val opt_model =
1.268 - Document_Model(buffer) match {
1.269 - case Some(model) => model.refresh; Some(model)
1.270 - case None =>
1.271 - Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
1.272 - case Some((dir, thy_name)) =>
1.273 - Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
1.274 - case None => None
1.275 - }
1.276 - }
1.277 - if (opt_model.isDefined) {
1.278 - for (text_area <- Isabelle.jedit_text_areas(buffer)) {
1.279 - if (Document_View(text_area).map(_.model) != opt_model)
1.280 - Document_View.init(opt_model.get, text_area)
1.281 - }
1.282 - }
1.283 - }
1.284 - }
1.285 -
1.286 - private def exit_model(buffer: Buffer)
1.287 - {
1.288 - Isabelle.swing_buffer_lock(buffer) {
1.289 - Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
1.290 - Document_Model.exit(buffer)
1.291 - }
1.292 - }
1.293 -
1.294 - private case class Init_Model(buffer: Buffer)
1.295 - private case class Exit_Model(buffer: Buffer)
1.296 - private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
1.297 - private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
1.298 -
1.299 - private val session_manager = actor {
1.300 - var ready = false
1.301 - loop {
1.302 - react {
1.303 - case phase: Session.Phase =>
1.304 - ready = phase == Session.Ready
1.305 - phase match {
1.306 - case Session.Failed =>
1.307 - Swing_Thread.now {
1.308 - val text = new scala.swing.TextArea(Isabelle.session.syslog())
1.309 - text.editable = false
1.310 - Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
1.311 - }
1.312 -
1.313 - case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
1.314 - case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
1.315 - case _ =>
1.316 - }
1.317 -
1.318 - case Init_Model(buffer) =>
1.319 - if (ready) init_model(buffer)
1.320 -
1.321 - case Exit_Model(buffer) =>
1.322 - exit_model(buffer)
1.323 -
1.324 - case Init_View(buffer, text_area) =>
1.325 - if (ready) {
1.326 - Isabelle.swing_buffer_lock(buffer) {
1.327 - Document_Model(buffer) match {
1.328 - case Some(model) => Document_View.init(model, text_area)
1.329 - case None =>
1.330 - }
1.331 - }
1.332 - }
1.333 -
1.334 - case Exit_View(buffer, text_area) =>
1.335 - Isabelle.swing_buffer_lock(buffer) {
1.336 - Document_View.exit(text_area)
1.337 - }
1.338 -
1.339 - case bad => System.err.println("session_manager: ignoring bad message " + bad)
1.340 - }
1.341 - }
1.342 - }
1.343 -
1.344 -
1.345 - /* main plugin plumbing */
1.346 -
1.347 - override def handleMessage(message: EBMessage)
1.348 - {
1.349 - message match {
1.350 - case msg: EditorStarted =>
1.351 - Isabelle.check_jvm()
1.352 - if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
1.353 -
1.354 - case msg: BufferUpdate
1.355 - if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
1.356 -
1.357 - val buffer = msg.getBuffer
1.358 - if (buffer != null) session_manager ! Init_Model(buffer)
1.359 -
1.360 - case msg: EditPaneUpdate
1.361 - if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
1.362 - msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
1.363 - msg.getWhat == EditPaneUpdate.CREATED ||
1.364 - msg.getWhat == EditPaneUpdate.DESTROYED) =>
1.365 -
1.366 - val edit_pane = msg.getEditPane
1.367 - val buffer = edit_pane.getBuffer
1.368 - val text_area = edit_pane.getTextArea
1.369 -
1.370 - if (buffer != null && text_area != null) {
1.371 - if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
1.372 - msg.getWhat == EditPaneUpdate.CREATED)
1.373 - session_manager ! Init_View(buffer, text_area)
1.374 - else
1.375 - session_manager ! Exit_View(buffer, text_area)
1.376 - }
1.377 -
1.378 - case msg: PropertiesChanged =>
1.379 - Swing_Thread.now {
1.380 - Isabelle.setup_tooltips()
1.381 - for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
1.382 - Document_View(text_area).get.extend_styles()
1.383 - }
1.384 - Isabelle.session.global_settings.event(Session.Global_Settings)
1.385 -
1.386 - case _ =>
1.387 - }
1.388 - }
1.389 -
1.390 - override def start()
1.391 - {
1.392 - Isabelle.setup_tooltips()
1.393 - Isabelle.system = new Isabelle_System
1.394 - Isabelle.system.install_fonts()
1.395 - Isabelle.session = new Session(Isabelle.system)
1.396 - Isabelle.session.phase_changed += session_manager
1.397 - }
1.398 -
1.399 - override def stop()
1.400 - {
1.401 - Isabelle.session.stop()
1.402 - Isabelle.session.phase_changed -= session_manager
1.403 - }
1.404 -}