src/Tools/jEdit/src/jedit/plugin.scala
author wenzelm
Tue Dec 08 16:30:20 2009 +0100 (2009-12-08)
changeset 34760 dc7f5e0d9d27
parent 34759 bfea7839d9e1
child 34762 0974378d235a
permissions -rw-r--r--
misc modernization of names;
     1 /*
     2  * Main Isabelle/jEdit plugin setup
     3  *
     4  * @author Johannes Hölzl, TU Munich
     5  * @author Fabian Immler, TU Munich
     6  * @author Makarius
     7  */
     8 
     9 package isabelle.jedit
    10 
    11 
    12 import java.io.{FileInputStream, IOException}
    13 import java.awt.Font
    14 import javax.swing.JScrollPane
    15 
    16 import scala.collection.mutable
    17 
    18 import isabelle.proofdocument.{Command, Proof_Document, Prover}
    19 import isabelle.Isabelle_System
    20 
    21 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    22 import org.gjt.sp.jedit.buffer.JEditBuffer
    23 import org.gjt.sp.jedit.textarea.JEditTextArea
    24 import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    25 
    26 
    27 object Isabelle
    28 {
    29   /* name */
    30 
    31   val NAME = "Isabelle"
    32 
    33 
    34   /* properties */
    35 
    36   val OPTION_PREFIX = "options.isabelle."
    37 
    38   object Property
    39   {
    40     def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
    41     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    42   }
    43 
    44   object Boolean_Property
    45   {
    46     def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
    47     def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    48   }
    49 
    50   object Int_Property
    51   {
    52     def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
    53     def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    54   }
    55 
    56 
    57   /* Isabelle system instance */
    58 
    59   var system: Isabelle_System = null
    60   def symbols = system.symbols
    61   lazy val completion = new Completion + symbols
    62 
    63 
    64   /* settings */
    65 
    66   def default_logic(): String =
    67   {
    68     val logic = Isabelle.Property("logic")
    69     if (logic != null) logic
    70     else system.getenv_strict("ISABELLE_LOGIC")
    71   }
    72 
    73 
    74   /* plugin instance */
    75 
    76   var plugin: Plugin = null
    77 
    78 
    79   /* running provers */
    80 
    81   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    82 }
    83 
    84 
    85 class Plugin extends EBPlugin
    86 {
    87   /* event buses */
    88 
    89   val state_update = new Event_Bus[Command]
    90 
    91 
    92   /* selected state */
    93 
    94   private var _selected_state: Command = null
    95   def selected_state = _selected_state
    96   def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
    97 
    98 
    99   /* mapping buffer <-> prover */
   100 
   101   private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
   102 
   103   private def install(view: View)
   104   {
   105     val buffer = view.getBuffer
   106     val prover_setup = new Prover_Setup(buffer)
   107     mapping.update(buffer, prover_setup)
   108     prover_setup.activate(view)
   109   }
   110 
   111   private def uninstall(view: View) =
   112     mapping.removeKey(view.getBuffer).get.deactivate
   113 
   114   def switch_active (view: View) =
   115     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   116     else install(view)
   117 
   118   def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
   119   def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   120 
   121 
   122   /* main plugin plumbing */
   123 
   124   override def handleMessage(msg: EBMessage)
   125   {
   126     msg match {
   127       case epu: EditPaneUpdate =>
   128         val buffer = epu.getEditPane.getBuffer
   129         epu.getWhat match {
   130           case EditPaneUpdate.BUFFER_CHANGED =>
   131             (mapping get buffer) map (_.theory_view.activate)
   132           case EditPaneUpdate.BUFFER_CHANGING =>
   133             if (buffer != null)
   134               (mapping get buffer) map (_.theory_view.deactivate)
   135           case _ =>
   136         }
   137       case _ =>
   138     }
   139   }
   140 
   141   override def start()
   142   {
   143     Isabelle.plugin = this
   144     Isabelle.system = new Isabelle_System
   145     if (!Isabelle.system.register_fonts())
   146       System.err.println("Failed to register Isabelle fonts")
   147   }
   148 
   149   override def stop()
   150   {
   151     // TODO: proper cleanup
   152     Isabelle.system = null
   153     Isabelle.plugin = null
   154   }
   155 }