src/Tools/jEdit/src/jedit/plugin.scala
author wenzelm
Sat Sep 18 14:28:42 2010 +0200 (2010-09-18)
changeset 39515 57ceabb0bb8e
parent 39241 e9a442606db3
child 39517 e036c67448e6
permissions -rw-r--r--
basic setup for prover session panel;
     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, 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.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
    23 import org.gjt.sp.jedit.gui.DockableWindowManager
    24 
    25 import org.gjt.sp.util.Log
    26 
    27 
    28 object Isabelle
    29 {
    30   /* plugin instance */
    31 
    32   var system: Isabelle_System = null
    33   var session: Session = null
    34 
    35 
    36   /* properties */
    37 
    38   val OPTION_PREFIX = "options.isabelle."
    39 
    40   object Property
    41   {
    42     def apply(name: String): String =
    43       jEdit.getProperty(OPTION_PREFIX + name)
    44     def apply(name: String, default: String): String =
    45       jEdit.getProperty(OPTION_PREFIX + name, default)
    46     def update(name: String, value: String) =
    47       jEdit.setProperty(OPTION_PREFIX + name, value)
    48   }
    49 
    50   object Boolean_Property
    51   {
    52     def apply(name: String): Boolean =
    53       jEdit.getBooleanProperty(OPTION_PREFIX + name)
    54     def apply(name: String, default: Boolean): Boolean =
    55       jEdit.getBooleanProperty(OPTION_PREFIX + name, default)
    56     def update(name: String, value: Boolean) =
    57       jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    58   }
    59 
    60   object Int_Property
    61   {
    62     def apply(name: String): Int =
    63       jEdit.getIntegerProperty(OPTION_PREFIX + name)
    64     def apply(name: String, default: Int): Int =
    65       jEdit.getIntegerProperty(OPTION_PREFIX + name, default)
    66     def update(name: String, value: Int) =
    67       jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    68   }
    69 
    70 
    71   /* font */
    72 
    73   def font_family(): String = jEdit.getProperty("view.font")
    74 
    75   def font_size(): Float =
    76     (jEdit.getIntegerProperty("view.fontsize", 16) *
    77       Int_Property("relative-font-size", 100)).toFloat / 100
    78 
    79 
    80   /* text area ranges */
    81 
    82   case class Gfx_Range(val x: Int, val y: Int, val length: Int)
    83 
    84   def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
    85   {
    86     val p = text_area.offsetToXY(range.start)
    87     val q = text_area.offsetToXY(range.stop)
    88     if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
    89     else None
    90   }
    91 
    92 
    93   /* tooltip markup */
    94 
    95   def tooltip(text: String): String =
    96     "<html><pre style=\"font-family: " + font_family() + "; font-size: " +
    97         Int_Property("tooltip-font-size", 10).toString + "px; \">" +  // FIXME proper scaling (!?)
    98       HTML.encode(text) + "</pre></html>"
    99 
   100   def tooltip_dismiss_delay(): Int =
   101     Int_Property("tooltip-dismiss-delay", 8000) max 500
   102 
   103   def setup_tooltips()
   104   {
   105     Swing_Thread.now {
   106       val manager = javax.swing.ToolTipManager.sharedInstance
   107       manager.setDismissDelay(tooltip_dismiss_delay())
   108     }
   109   }
   110 
   111 
   112   /* icons */
   113 
   114   def load_icon(name: String): javax.swing.Icon =
   115   {
   116     val icon = GUIUtilities.loadIcon(name)
   117     if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
   118       Log.log(Log.ERROR, icon, "Bad icon: " + name);
   119     icon
   120   }
   121 
   122 
   123   /* settings */
   124 
   125   def default_logic(): String =
   126   {
   127     val logic = system.getenv("JEDIT_LOGIC")
   128     if (logic != "") logic
   129     else system.getenv_strict("ISABELLE_LOGIC")
   130   }
   131 
   132   def isabelle_args(): List[String] =
   133   {
   134     val modes = system.getenv("JEDIT_PRINT_MODE").split(",").toList.map("-m" + _)
   135     val logic = {
   136       val logic = Property("logic")
   137       if (logic != null && logic != "") logic
   138       else default_logic()
   139     }
   140     modes ++ List(logic)
   141   }
   142 
   143 
   144   /* main jEdit components */
   145 
   146   def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
   147 
   148   def jedit_views(): Iterator[View] = jEdit.getViews().iterator
   149 
   150   def jedit_text_areas(view: View): Iterator[JEditTextArea] =
   151     view.getEditPanes().iterator.map(_.getTextArea)
   152 
   153   def jedit_text_areas(): Iterator[JEditTextArea] =
   154     jedit_views().flatMap(jedit_text_areas(_))
   155 
   156   def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
   157     jedit_text_areas().filter(_.getBuffer == buffer)
   158 
   159   def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   160   {
   161     try { buffer.readLock(); body }
   162     finally { buffer.readUnlock() }
   163   }
   164 
   165   def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
   166     Swing_Thread.now { buffer_lock(buffer) { body } }
   167 
   168 
   169   /* dockable windows */
   170 
   171   private def wm(view: View): DockableWindowManager = view.getDockableWindowManager
   172 
   173   def docked_session(view: View): Option[Session_Dockable] =
   174     wm(view).getDockableWindow("isabelle-session") match {
   175       case dockable: Session_Dockable => Some(dockable)
   176       case _ => None
   177     }
   178 
   179   def docked_output(view: View): Option[Output_Dockable] =
   180     wm(view).getDockableWindow("isabelle-output") match {
   181       case dockable: Output_Dockable => Some(dockable)
   182       case _ => None
   183     }
   184 
   185   def docked_raw_output(view: View): Option[Raw_Output_Dockable] =
   186     wm(view).getDockableWindow("isabelle-raw-output") match {
   187       case dockable: Raw_Output_Dockable => Some(dockable)
   188       case _ => None
   189     }
   190 
   191   def docked_protocol(view: View): Option[Protocol_Dockable] =
   192     wm(view).getDockableWindow("isabelle-protocol") match {
   193       case dockable: Protocol_Dockable => Some(dockable)
   194       case _ => None
   195     }
   196 
   197 
   198   /* manage prover */  // FIXME async!?
   199 
   200   private def prover_started(view: View): Boolean =
   201   {
   202     val timeout = Int_Property("startup-timeout") max 1000
   203     session.started(timeout, Isabelle.isabelle_args()) match {
   204       case Some(err) =>
   205         val text = new JTextArea(err); text.setEditable(false)
   206         Library.error_dialog(view, null, "Failed to start Isabelle process", text)
   207         false
   208       case None => true
   209     }
   210   }
   211 
   212 
   213   /* activation */
   214 
   215   def activate_buffer(view: View, buffer: Buffer)
   216   {
   217     if (prover_started(view)) {
   218       // FIXME proper error handling
   219       val (_, thy_name) = Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath))
   220 
   221       val model = Document_Model.init(session, buffer, thy_name)
   222       for (text_area <- jedit_text_areas(buffer))
   223         Document_View.init(model, text_area)
   224     }
   225   }
   226 
   227   def deactivate_buffer(buffer: Buffer)
   228   {
   229     session.stop()  // FIXME not yet
   230 
   231     for (text_area <- jedit_text_areas(buffer))
   232       Document_View.exit(text_area)
   233     Document_Model.exit(buffer)
   234   }
   235 
   236   def switch_active(view: View) =
   237   {
   238     val buffer = view.getBuffer
   239     if (Document_Model(buffer).isDefined) deactivate_buffer(buffer)
   240     else activate_buffer(view, buffer)
   241   }
   242 
   243   def is_active(view: View): Boolean =
   244     Document_Model(view.getBuffer).isDefined
   245 }
   246 
   247 
   248 class Plugin extends EBPlugin
   249 {
   250   /* main plugin plumbing */
   251 
   252   override def handleMessage(message: EBMessage)
   253   {
   254     message match {
   255       case msg: BufferUpdate
   256         if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
   257         Document_Model(msg.getBuffer) match {
   258           case Some(model) => model.refresh()
   259           case _ =>
   260         }
   261 
   262       case msg: EditPaneUpdate =>
   263         val edit_pane = msg.getEditPane
   264         val buffer = edit_pane.getBuffer
   265         val text_area = edit_pane.getTextArea
   266 
   267         def init_view()
   268         {
   269           Document_Model(buffer) match {
   270             case Some(model) => Document_View.init(model, text_area)
   271             case None =>
   272           }
   273         }
   274         def exit_view()
   275         {
   276           if (Document_View(text_area).isDefined)
   277             Document_View.exit(text_area)
   278         }
   279         msg.getWhat match {
   280           case EditPaneUpdate.BUFFER_CHANGED => exit_view(); init_view()
   281           case EditPaneUpdate.CREATED => init_view()
   282           case EditPaneUpdate.DESTROYED => exit_view()
   283           case _ =>
   284         }
   285 
   286       case msg: PropertiesChanged =>
   287         Swing_Thread.now {
   288           for (text_area <- Isabelle.jedit_text_areas if Document_View(text_area).isDefined)
   289             Document_View(text_area).get.extend_styles()
   290 
   291           Isabelle.setup_tooltips()
   292         }
   293 
   294         Isabelle.session.global_settings.event(Session.Global_Settings)
   295 
   296       case _ =>
   297     }
   298   }
   299 
   300   override def start()
   301   {
   302     Isabelle.system = new Isabelle_System
   303     Isabelle.system.install_fonts()
   304     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   305 
   306     Isabelle.setup_tooltips()
   307   }
   308 
   309   override def stop()  // FIXME fragile
   310   {
   311     Isabelle.session.stop()  // FIXME dialog!?
   312     Isabelle.session = null
   313   }
   314 }