src/Tools/jEdit/src/jedit/plugin.scala
changeset 34759 bfea7839d9e1
parent 34751 6ed1b3701459
child 34760 dc7f5e0d9d27
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Tue Dec 08 14:49:01 2009 +0100
     1.3 @@ -0,0 +1,155 @@
     1.4 +/*
     1.5 + * Main Isabelle/jEdit plugin setup
     1.6 + *
     1.7 + * @author Johannes Hölzl, TU Munich
     1.8 + * @author Fabian Immler, TU Munich
     1.9 + */
    1.10 +
    1.11 +package isabelle.jedit
    1.12 +
    1.13 +
    1.14 +import java.io.{FileInputStream, IOException}
    1.15 +import java.awt.Font
    1.16 +import javax.swing.JScrollPane
    1.17 +
    1.18 +import scala.collection.mutable
    1.19 +
    1.20 +import isabelle.prover.{Prover, Command}
    1.21 +import isabelle.proofdocument.ProofDocument
    1.22 +import isabelle.Isabelle_System
    1.23 +
    1.24 +import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    1.25 +import org.gjt.sp.jedit.buffer.JEditBuffer
    1.26 +import org.gjt.sp.jedit.textarea.JEditTextArea
    1.27 +import org.gjt.sp.jedit.msg.{EditPaneUpdate, PropertiesChanged}
    1.28 +
    1.29 +
    1.30 +object Isabelle
    1.31 +{
    1.32 +  /* name */
    1.33 +
    1.34 +  val NAME = "Isabelle"
    1.35 +
    1.36 +
    1.37 +  /* properties */
    1.38 +
    1.39 +  val OPTION_PREFIX = "options.isabelle."
    1.40 +
    1.41 +  object Property
    1.42 +  {
    1.43 +    def apply(name: String): String = jEdit.getProperty(OPTION_PREFIX + name)
    1.44 +    def update(name: String, value: String) = jEdit.setProperty(OPTION_PREFIX + name, value)
    1.45 +  }
    1.46 +
    1.47 +  object Boolean_Property
    1.48 +  {
    1.49 +    def apply(name: String): Boolean = jEdit.getBooleanProperty(OPTION_PREFIX + name)
    1.50 +    def update(name: String, value: Boolean) = jEdit.setBooleanProperty(OPTION_PREFIX + name, value)
    1.51 +  }
    1.52 +
    1.53 +  object Int_Property
    1.54 +  {
    1.55 +    def apply(name: String): Int = jEdit.getIntegerProperty(OPTION_PREFIX + name)
    1.56 +    def update(name: String, value: Int) = jEdit.setIntegerProperty(OPTION_PREFIX + name, value)
    1.57 +  }
    1.58 +
    1.59 +
    1.60 +  /* Isabelle system instance */
    1.61 +
    1.62 +  var system: Isabelle_System = null
    1.63 +  def symbols = system.symbols
    1.64 +  lazy val completion = new Completion + symbols
    1.65 +
    1.66 +
    1.67 +  /* settings */
    1.68 +
    1.69 +  def default_logic(): String =
    1.70 +  {
    1.71 +    val logic = Isabelle.Property("logic")
    1.72 +    if (logic != null) logic
    1.73 +    else system.getenv_strict("ISABELLE_LOGIC")
    1.74 +  }
    1.75 +
    1.76 +
    1.77 +  /* plugin instance */
    1.78 +
    1.79 +  var plugin: Plugin = null
    1.80 +
    1.81 +
    1.82 +  /* running provers */
    1.83 +
    1.84 +  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    1.85 +}
    1.86 +
    1.87 +
    1.88 +class Plugin extends EBPlugin
    1.89 +{
    1.90 +  /* event buses */
    1.91 +
    1.92 +  val state_update = new Event_Bus[Command]
    1.93 +
    1.94 +
    1.95 +  /* selected state */
    1.96 +
    1.97 +  private var _selected_state: Command = null
    1.98 +  def selected_state = _selected_state
    1.99 +  def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
   1.100 +
   1.101 +
   1.102 +  /* mapping buffer <-> prover */
   1.103 +
   1.104 +  private val mapping = new mutable.HashMap[JEditBuffer, ProverSetup]
   1.105 +
   1.106 +  private def install(view: View)
   1.107 +  {
   1.108 +    val buffer = view.getBuffer
   1.109 +    val prover_setup = new ProverSetup(buffer)
   1.110 +    mapping.update(buffer, prover_setup)
   1.111 +    prover_setup.activate(view)
   1.112 +  }
   1.113 +
   1.114 +  private def uninstall(view: View) =
   1.115 +    mapping.removeKey(view.getBuffer).get.deactivate
   1.116 +
   1.117 +  def switch_active (view: View) =
   1.118 +    if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   1.119 +    else install(view)
   1.120 +
   1.121 +  def prover_setup(buffer: JEditBuffer): Option[ProverSetup] = mapping.get(buffer)
   1.122 +  def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   1.123 +
   1.124 +
   1.125 +  /* main plugin plumbing */
   1.126 +
   1.127 +  override def handleMessage(msg: EBMessage)
   1.128 +  {
   1.129 +    msg match {
   1.130 +      case epu: EditPaneUpdate =>
   1.131 +        val buffer = epu.getEditPane.getBuffer
   1.132 +        epu.getWhat match {
   1.133 +          case EditPaneUpdate.BUFFER_CHANGED =>
   1.134 +            (mapping get buffer) map (_.theory_view.activate)
   1.135 +          case EditPaneUpdate.BUFFER_CHANGING =>
   1.136 +            if (buffer != null)
   1.137 +              (mapping get buffer) map (_.theory_view.deactivate)
   1.138 +          case _ =>
   1.139 +        }
   1.140 +      case _ =>
   1.141 +    }
   1.142 +  }
   1.143 +
   1.144 +  override def start()
   1.145 +  {
   1.146 +    Isabelle.plugin = this
   1.147 +    Isabelle.system = new Isabelle_System
   1.148 +    if (!Isabelle.system.register_fonts())
   1.149 +      System.err.println("Failed to register Isabelle fonts")
   1.150 +  }
   1.151 +
   1.152 +  override def stop()
   1.153 +  {
   1.154 +    // TODO: proper cleanup
   1.155 +    Isabelle.system = null
   1.156 +    Isabelle.plugin = null
   1.157 +  }
   1.158 +}