src/Tools/jEdit/src/jedit/Plugin.scala
author wenzelm
Tue Jun 23 20:49:56 2009 +0200 (2009-06-23)
changeset 34612 5a03dc7a19e1
parent 34503 7d0726f19d04
child 34615 5e61055bf35b
permissions -rw-r--r--
fall back on Isabelle system completion (symbols only);
tuned;
     1 /*
     2  * Main Isabelle/jEdit plugin setup
     3  *
     4  * @author Johannes Hölzl, TU Munich
     5  * @author Fabian Immler, TU Munich
     6  */
     7 
     8 package isabelle.jedit
     9 
    10 
    11 import java.io.{FileInputStream, IOException}
    12 import java.awt.Font
    13 import javax.swing.JScrollPane
    14 
    15 import scala.collection.mutable
    16 
    17 import isabelle.prover.{Prover, Command}
    18 import isabelle.IsabelleSystem
    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   // name
    28   val NAME = "Isabelle"
    29   val VFS_PREFIX = "isabelle:"
    30 
    31   // properties
    32   object Property {
    33     private val OPTION_PREFIX = "options.isabelle."
    34     def apply(name: String) = jEdit.getProperty(OPTION_PREFIX + name)
    35     def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    36   }
    37 
    38   // Isabelle system instance
    39   var system: IsabelleSystem = null
    40   def symbols = system.symbols
    41   lazy val completion = new Completion + symbols
    42 
    43   // settings
    44   def default_logic = {
    45     val logic = Isabelle.Property("logic")
    46     if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC")
    47   }
    48 
    49   // plugin instance
    50   var plugin: Plugin = null
    51 
    52   // running provers
    53   def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    54 }
    55 
    56 
    57 class Plugin extends EBPlugin {
    58 
    59   // Isabelle font
    60 
    61   var font: Font = null
    62   val font_changed = new EventBus[Font]
    63 
    64   def set_font(path: String, size: Float) {
    65     font = Font.createFont(Font.TRUETYPE_FONT, new FileInputStream(path)).
    66       deriveFont(Font.PLAIN, size)
    67     font_changed.event(font)
    68   }
    69 
    70 
    71   /* unique ids */  // FIXME specific to "session" (!??)
    72 
    73   private var id_count: BigInt = 0
    74   def id() : String = synchronized { id_count += 1; "editor:" + id_count }
    75 
    76 
    77   // mapping buffer <-> prover
    78 
    79   private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
    80 
    81   private def install(view: View) {
    82     val buffer = view.getBuffer
    83     val prover_setup = new ProverSetup(buffer)
    84     mapping.update(buffer, prover_setup)
    85     prover_setup.activate(view)
    86   }
    87 
    88   private def uninstall(view: View) =
    89     mapping.removeKey(view.getBuffer).get.deactivate
    90 
    91   def switch_active (view : View) =
    92     if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
    93     else install(view)
    94 
    95   def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
    96   def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
    97   
    98   
    99   // main plugin plumbing
   100 
   101   override def handleMessage(msg: EBMessage) = msg match {
   102     case epu: EditPaneUpdate => epu.getWhat match {
   103       case EditPaneUpdate.BUFFER_CHANGED =>
   104         mapping get epu.getEditPane.getBuffer match {
   105           //only activate 'isabelle'-buffers!
   106           case None =>
   107           case Some(prover_setup) => 
   108             prover_setup.theory_view.activate
   109             val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("isabelle-output")
   110             if (dockable != null) {
   111               val output_dockable = dockable.asInstanceOf[OutputDockable]
   112               if (output_dockable.getComponent(0) != prover_setup.output_text_view ) {
   113                 output_dockable.asInstanceOf[OutputDockable].removeAll
   114                 output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
   115                 output_dockable.revalidate
   116               }
   117             }
   118         }
   119       case EditPaneUpdate.BUFFER_CHANGING =>
   120         val buffer = epu.getEditPane.getBuffer
   121         if (buffer != null) mapping get buffer match {
   122           //only deactivate 'isabelle'-buffers!
   123           case None =>
   124           case Some(prover_setup) => prover_setup.theory_view.deactivate
   125         }
   126       case _ =>
   127     }
   128     case _ =>
   129   }
   130 
   131   override def start() {
   132     Isabelle.system = new IsabelleSystem
   133     Isabelle.plugin = this
   134     
   135     if (Isabelle.Property("font-path") != null && Isabelle.Property("font-size") != null)
   136       try {
   137         set_font(Isabelle.Property("font-path"), Isabelle.Property("font-size").toFloat)
   138       }
   139       catch {
   140         case e: NumberFormatException =>
   141       }
   142   }
   143   
   144   override def stop() {
   145     // TODO: proper cleanup
   146     Isabelle.system = null
   147     Isabelle.plugin = null
   148   }
   149 }