src/Tools/jEdit/src/jedit/plugin.scala
author wenzelm
Mon Aug 23 17:35:47 2010 +0200 (2010-08-23)
changeset 38640 105d1f112da5
parent 38222 dac5fa0ac971
child 38843 d95522496593
permissions -rw-r--r--
sporadic locking of jEdit buffer;
     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   def buffer_read_lock[A](buffer: JEditBuffer)(body: => A): A =
   122   {
   123     try { buffer.readLock(); body }
   124     finally { buffer.readUnlock() }
   125   }
   126 
   127 
   128   /* dockable windows */
   129 
   130   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
   131 
   132   def docked_output(view: View): Option[Output_Dockable] =
   133     wm(view).getDockableWindow("isabelle-output") match {
   134       case dockable: Output_Dockable => Some(dockable)
   135       case _ => None
   136     }
   137 
   138   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
   139     wm(view).getDockableWindow("isabelle-raw-output") match {
   140       case dockable: Raw_Output_Dockable => Some(dockable)
   141       case _ => None
   142     }
   143 
   144   def docked_protocol(view: View): Option[Protocol_Dockable] =
   145     wm(view).getDockableWindow("isabelle-protocol") match {
   146       case dockable: Protocol_Dockable => Some(dockable)
   147       case _ => None
   148     }
   149 
   150 
   151   /* manage prover */  // FIXME async!?
   152 
   153   private def prover_started(view: View): Boolean =
   154   {
   155     val timeout = Int_Property("startup-timeout") max 1000
   156     session.started(timeout, Isabelle.isabelle_args()) match {
   157       case Some(err) =>
   158         val text = new JTextArea(err); text.setEditable(false)
   159         Library.error_dialog(view, null, "Failed to start Isabelle process", text)
   160         false
   161       case None => true
   162     }
   163   }
   164 
   165 
   166   /* activation */
   167 
   168   def activate_buffer(view: View, buffer: Buffer)
   169   {
   170     if (prover_started(view)) {
   171       // FIXME proper error handling
   172       val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
   173 
   174       val model = Document_Model.init(session, buffer, thy_name)
   175       for (text_area <- jedit_text_areas(buffer))
   176         Document_View.init(model, text_area)
   177     }
   178   }
   179 
   180   def deactivate_buffer(buffer: Buffer)
   181   {
   182     session.stop()  // FIXME not yet
   183 
   184     for (text_area <- jedit_text_areas(buffer))
   185       Document_View.exit(text_area)
   186     Document_Model.exit(buffer)
   187   }
   188 
   189   def switch_active(view: View) =
   190   {
   191     val buffer = view.getBuffer
   192     if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
   193     else activate_buffer(view, buffer)
   194   }
   195 
   196   def is_active(view: View): Boolean =
   197     Document_Model(view.getBuffer).isDefined
   198 }
   199 
   200 
   201 class Plugin extends EBPlugin
   202 {
   203   /* main plugin plumbing */
   204 
   205   override def handleMessage(message: EBMessage)
   206   {
   207     message match {
   208       case msg: BufferUpdate
   209         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   210         Document_Model(msg.getBuffer) match {
   211           case Some(model) => model.refresh()
   212           case _ =>
   213         }
   214 
   215       case msg: EditPaneUpdate =>
   216         val edit_pane = msg.getEditPane
   217         val buffer = edit_pane.getBuffer
   218         val text_area = edit_pane.getTextArea
   219 
   220         def init_view()
   221         {
   222           Document_Model(buffer) match {
   223             case Some(model) => Document_View.init(model, text_area)
   224             case None =>
   225           }
   226         }
   227         def exit_view()
   228         {
   229           if (Document_View(text_area).isDefined)
   230             Document_View.exit(text_area)
   231         }
   232         msg.getWhat match {
   233           case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
   234           case EditPaneUpdate.CREATED => init_view()
   235           case EditPaneUpdate.DESTROYED => exit_view()
   236           case _ =>
   237         }
   238 
   239       case msg: PropertiesChanged =>
   240         Swing_Thread.now {
   241           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
   242             Document_View(text_area).get.extend_styles()
   243         }
   244 
   245         Isabelle.session.global_settings.event(Session.Global_Settings)
   246 
   247       case _ =>
   248     }
   249   }
   250 
   251   override def start()
   252   {
   253     Isabelle.system = new Isabelle_System
   254     Isabelle.system.install_fonts()
   255     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   256   }
   257 
   258   override def stop()
   259   {
   260     Isabelle.session.stop()  // FIXME dialog!?
   261     Isabelle.session = null
   262     Isabelle.system = null
   263   }
   264 }