src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34759 bfea7839d9e1
parent 34758 710e3a9a4c95
child 34760 dc7f5e0d9d27
     1.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala	Tue Dec 08 14:29:29 2009 +0100
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,155 +0,0 @@
     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 -}