src/Tools/jEdit/src/jedit/plugin.scala
author wenzelm
Sat Aug 07 13:19:48 2010 +0200 (2010-08-07)
changeset 38221 e0f00f0945b4
parent 37557 1ae272fd4082
child 38222 dac5fa0ac971
permissions -rw-r--r--
misc tuning and clarification;
     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 import javax.swing.JTextArea
    15 
    16 import scala.collection.mutable
    17 
    18 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    19 import org.gjt.sp.jedit.buffer.JEditBuffer
    20 import org.gjt.sp.jedit.textarea.JEditTextArea
    21 import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
    22 import org.gjt.sp.jedit.gui.DockableWindowManager
    23 
    24 
    25 object Isabelle
    26 {
    27   /* plugin instance */
    28 
    29   var system: Isabelle_System = null
    30   var session: Session = null
    31 
    32 
    33   /* properties */
    34 
    35   val OPTION_PREFIX = "options.isabelle."
    36 
    37   object Property
    38   {
    39     def apply(name: String): String =
    40       jEdit.getProperty(OPTION_PREFIX + name)
    41     def apply(name: String, default: String): String =
    42       jEdit.getProperty(OPTION_PREFIX + name, default)
    43     def update(name: String, value: String) =
    44       jEdit.setProperty(OPTION_PREFIX + name, value)
    45   }
    46 
    47   object Boolean_Property
    48   {
    49     def apply(name: String): Boolean =
    50       jEdit.getBooleanProperty(OPTION_PREFIX + name)
    51     def apply(name: String, default: Boolean): Boolean =
    52       jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
    53     def update(name: String, value: Boolean) =
    54       jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    55   }
    56 
    57   object Int_Property
    58   {
    59     def apply(name: String): Int =
    60       jEdit.getIntegerProperty(OPTION_PREFIX + name)
    61     def apply(name: String, default: Int): Int =
    62       jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
    63     def update(name: String, value: Int) =
    64       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    65   }
    66 
    67 
    68   /* font */
    69 
    70   def font_family(): String = jEdit.getProperty("view.font")
    71 
    72   def font_size(): Float =
    73     (jEdit.getIntegerProperty("view.fontsize", 16) *
    74       Int_Property("relative-font-size", 100)).toFloat / 100
    75 
    76 
    77   /* tooltip markup */
    78 
    79   def tooltip(text: String): String =
    80     "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
    81         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
    82       HTML.encode(text) + "</pre></html>"
    83 
    84 
    85   /* settings */
    86 
    87   def default_logic(): String =
    88   {
    89     val logic = system.getenv("JEDIT_LOGIC")
    90     if (logic != "") logic
    91     else system.getenv_strict("ISABELLE_LOGIC")
    92   }
    93 
    94   def isabelle_args(): List[String] =
    95   {
    96     val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
    97     val logic = {
    98       val logic = Property("logic")
    99       if (logic != null && logic != "") logic
   100       else default_logic()
   101     }
   102     modes ++ List(logic)
   103   }
   104 
   105 
   106   /* main jEdit components */
   107 
   108   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   109 
   110   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   111 
   112   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
   113     view.getEditPanes().iterator.map(_.getTextArea)
   114 
   115   def jedit_text_areas(): Iterator[JEditTextArea] =
   116     jedit_views().flatMap(jedit_text_areas(_))
   117 
   118   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
   119     jedit_text_areas().filter(_.getBuffer == buffer)
   120 
   121 
   122   /* dockable windows */
   123 
   124   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
   125 
   126   def docked_output(view: View): Option[Output_Dockable] =
   127     wm(view).getDockableWindow("isabelle-output") match {
   128       case dockable: Output_Dockable => Some(dockable)
   129       case _ => None
   130     }
   131 
   132   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
   133     wm(view).getDockableWindow("isabelle-raw-output") match {
   134       case dockable: Raw_Output_Dockable => Some(dockable)
   135       case _ => None
   136     }
   137 
   138   def docked_protocol(view: View): Option[Protocol_Dockable] =
   139     wm(view).getDockableWindow("isabelle-protocol") match {
   140       case dockable: Protocol_Dockable => Some(dockable)
   141       case _ => None
   142     }
   143 
   144 
   145   /* manage prover */  // FIXME async!?
   146 
   147   private def prover_started(view: View): Boolean =
   148   {
   149     val timeout = Int_Property("startup-timeout") max 1000
   150     session.started(timeout, Isabelle.isabelle_args()) match {
   151       case Some(err) =>
   152         val text = new JTextArea(err); text.setEditable(false)
   153         Library.error_dialog(view, null, "Failed to start Isabelle process", text)
   154         false
   155       case None => true
   156     }
   157   }
   158 
   159 
   160   /* activation */
   161 
   162   def activate_buffer(view: View, buffer: Buffer)
   163   {
   164     if (prover_started(view)) {
   165       val model = Document_Model.init(session, buffer)
   166       for (text_area <- jedit_text_areas(buffer))
   167         Document_View.init(model, text_area)
   168     }
   169   }
   170 
   171   def deactivate_buffer(buffer: Buffer)
   172   {
   173     session.stop()  // FIXME not yet
   174 
   175     for (text_area <- jedit_text_areas(buffer))
   176       Document_View.exit(text_area)
   177     Document_Model.exit(buffer)
   178   }
   179 
   180   def switch_active(view: View) =
   181   {
   182     val buffer = view.getBuffer
   183     if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
   184     else activate_buffer(view, buffer)
   185   }
   186 
   187   def is_active(view: View): Boolean =
   188     Document_Model(view.getBuffer).isDefined
   189 }
   190 
   191 
   192 class Plugin extends EBPlugin
   193 {
   194   /* main plugin plumbing */
   195 
   196   override def handleMessage(message: EBMessage)
   197   {
   198     message match {
   199       case msg: BufferUpdate
   200         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   201         Document_Model(msg.getBuffer) match {
   202           case Some(model) => model.refresh()
   203           case _ =>
   204         }
   205 
   206       case msg: EditPaneUpdate =>
   207         val edit_pane = msg.getEditPane
   208         val buffer = edit_pane.getBuffer
   209         val text_area = edit_pane.getTextArea
   210 
   211         def init_view()
   212         {
   213           Document_Model(buffer) match {
   214             case Some(model) => Document_View.init(model, text_area)
   215             case None =>
   216           }
   217         }
   218         def exit_view()
   219         {
   220           if (Document_View(text_area).isDefined)
   221             Document_View.exit(text_area)
   222         }
   223         msg.getWhat match {
   224           case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
   225           case EditPaneUpdate.CREATED => init_view()
   226           case EditPaneUpdate.DESTROYED => exit_view()
   227           case _ =>
   228         }
   229 
   230       case msg: PropertiesChanged =>
   231         Swing_Thread.now {
   232           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
   233             Document_View(text_area).get.extend_styles()
   234         }
   235 
   236         Isabelle.session.global_settings.event(Session.Global_Settings)
   237 
   238       case _ =>
   239     }
   240   }
   241 
   242   override def start()
   243   {
   244     Isabelle.system = new Isabelle_System
   245     Isabelle.system.install_fonts()
   246     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   247   }
   248 
   249   override def stop()
   250   {
   251     Isabelle.session.stop()  // FIXME dialog!?
   252     Isabelle.session = null
   253     Isabelle.system = null
   254   }
   255 }