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