src/Tools/jEdit/src/plugin.scala
changeset 43282 5d294220ca43
parent 41537 3837045cc8a1
child 43390 7ee98a3802af
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Jun 08 17:42:07 2011 +0200
     1.3 @@ -0,0 +1,401 @@
     1.4 +/*  Title:      Tools/jEdit/src/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 +}