src/Tools/jEdit/src/jedit/plugin.scala
author wenzelm
Thu Dec 10 22:15:19 2009 +0100 (2009-12-10 ago)
changeset 34777 91d6089cef88
parent 34774 1fa466333361
child 34779 d1040b77b189
permissions -rw-r--r--
class Session models full session, with or without prover process (cf. heaps, browser_info);
replaced Prover by Session, with a singleton instance in Isabelle plugin (shared by all active buffers);
misc cleanup of Session vs. Plugin instance;
eliminated Prover_Setup -- maintain mapping of JEditBuffer <-> Theory_View directly;
misc tuning and simplification;
     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 isabelle.proofdocument.{Session, Theory_View}
    13 
    14 import java.io.{FileInputStream, IOException}
    15 import java.awt.Font
    16 import javax.swing.JScrollPane
    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 
    25 
    26 object Isabelle
    27 {
    28   /* name */
    29 
    30   val NAME = "Isabelle"
    31 
    32 
    33   /* properties */
    34 
    35   val OPTION_PREFIX = "options.isabelle."
    36 
    37   object Property
    38   {
    39     def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
    40     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    41   }
    42 
    43   object Boolean_Property
    44   {
    45     def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
    46     def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    47   }
    48 
    49   object Int_Property
    50   {
    51     def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
    52     def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    53   }
    54 
    55 
    56   /* settings */
    57 
    58   def get_logic(): String =
    59   {
    60     val logic = Isabelle.Property("logic")
    61     if (logic != null) logic
    62     else system.getenv_strict("ISABELLE_LOGIC")
    63   }
    64 
    65 
    66   /* plugin instance */
    67 
    68   var plugin: Plugin = null
    69   var system: Isabelle_System = null
    70   var session: Session = null
    71 }
    72 
    73 
    74 class Plugin extends EBPlugin
    75 {
    76   /* mapping buffer <-> theory view */
    77 
    78   private var mapping = Map[JEditBuffer, Theory_View]()
    79 
    80   private def install(view: View)
    81   {
    82     val text_area = view.getTextArea
    83     val buffer = view.getBuffer
    84 
    85  
    86     val theory_view = new Theory_View(Isabelle.session, text_area)   // FIXME multiple text areas!?
    87     mapping += (buffer -> theory_view)
    88 
    89     Isabelle.session.start(Isabelle.get_logic())
    90     theory_view.activate()
    91     Isabelle.session.begin_document(buffer.getName)
    92   }
    93 
    94   private def uninstall(view: View)
    95   {
    96     val buffer = view.getBuffer
    97     mapping(buffer).deactivate
    98     mapping -= buffer
    99   }
   100 
   101   def switch_active(view: View) =
   102     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   103     else install(view)
   104 
   105   def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer)
   106   def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   107 
   108 
   109   /* main plugin plumbing */
   110 
   111   override def handleMessage(message: EBMessage)
   112   {
   113     message match {
   114       case msg: EditPaneUpdate =>
   115         val buffer = msg.getEditPane.getBuffer
   116         msg.getWhat match {
   117           case EditPaneUpdate.BUFFER_CHANGED =>
   118             theory_view(buffer)map(_.activate)
   119           case EditPaneUpdate.BUFFER_CHANGING =>
   120             if (buffer != null)
   121               theory_view(buffer).map(_.deactivate)
   122           case _ =>
   123         }
   124       case msg: PropertiesChanged =>
   125         Isabelle.session.global_settings.event(())
   126       case _ =>
   127     }
   128   }
   129 
   130   override def start()
   131   {
   132     Isabelle.plugin = this
   133     Isabelle.system = new Isabelle_System
   134     Isabelle.system.install_fonts()
   135     Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   136   }
   137 
   138   override def stop()
   139   {
   140     Isabelle.session.stop()  // FIXME dialog!?
   141     Isabelle.session = null
   142     Isabelle.system = null
   143     Isabelle.plugin = null
   144   }
   145 }