src/Tools/jEdit/src/jedit/plugin.scala
changeset 34777 91d6089cef88
parent 34774 1fa466333361
child 34779 d1040b77b189
     1.1 --- a/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 10 14:23:28 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/plugin.scala	Thu Dec 10 22:15:19 2009 +0100
     1.3 @@ -9,15 +9,14 @@
     1.4  package isabelle.jedit
     1.5  
     1.6  
     1.7 +import isabelle.proofdocument.{Session, Theory_View}
     1.8 +
     1.9  import java.io.{FileInputStream, IOException}
    1.10  import java.awt.Font
    1.11  import javax.swing.JScrollPane
    1.12  
    1.13  import scala.collection.mutable
    1.14  
    1.15 -import isabelle.proofdocument.{Command, Proof_Document, Prover}
    1.16 -import isabelle.Isabelle_System
    1.17 -
    1.18  import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
    1.19  import org.gjt.sp.jedit.buffer.JEditBuffer
    1.20  import org.gjt.sp.jedit.textarea.JEditTextArea
    1.21 @@ -54,16 +53,9 @@
    1.22    }
    1.23  
    1.24  
    1.25 -  /* Isabelle system instance */
    1.26 -
    1.27 -  var system: Isabelle_System = null
    1.28 -  def symbols = system.symbols
    1.29 -  lazy val completion = new Completion + symbols
    1.30 -
    1.31 -
    1.32    /* settings */
    1.33  
    1.34 -  def default_logic(): String =
    1.35 +  def get_logic(): String =
    1.36    {
    1.37      val logic = Isabelle.Property("logic")
    1.38      if (logic != null) logic
    1.39 @@ -74,51 +66,44 @@
    1.40    /* plugin instance */
    1.41  
    1.42    var plugin: Plugin = null
    1.43 -
    1.44 -
    1.45 -  /* running provers */
    1.46 -
    1.47 -  def prover_setup(buffer: JEditBuffer) = plugin.prover_setup(buffer)
    1.48 +  var system: Isabelle_System = null
    1.49 +  var session: Session = null
    1.50  }
    1.51  
    1.52  
    1.53  class Plugin extends EBPlugin
    1.54  {
    1.55 -  /* event buses */
    1.56 -
    1.57 -  val properties_changed = new Event_Bus[Unit]
    1.58 -  val raw_results = new Event_Bus[Isabelle_Process.Result]
    1.59 -  val state_update = new Event_Bus[Command]
    1.60 -
    1.61 -
    1.62 -  /* selected state */
    1.63 +  /* mapping buffer <-> theory view */
    1.64  
    1.65 -  private var _selected_state: Command = null
    1.66 -  def selected_state = _selected_state
    1.67 -  def selected_state_=(state: Command) { _selected_state = state; state_update.event(state) }
    1.68 -
    1.69 -
    1.70 -  /* mapping buffer <-> prover */
    1.71 -
    1.72 -  private val mapping = new mutable.HashMap[JEditBuffer, Prover_Setup]
    1.73 +  private var mapping = Map[JEditBuffer, Theory_View]()
    1.74  
    1.75    private def install(view: View)
    1.76    {
    1.77 +    val text_area = view.getTextArea
    1.78      val buffer = view.getBuffer
    1.79 -    val prover_setup = new Prover_Setup(buffer)
    1.80 -    mapping.update(buffer, prover_setup)
    1.81 -    prover_setup.activate(view)
    1.82 +
    1.83 + 
    1.84 +    val theory_view = new Theory_View(Isabelle.session, text_area)   // FIXME multiple text areas!?
    1.85 +    mapping += (buffer -> theory_view)
    1.86 +
    1.87 +    Isabelle.session.start(Isabelle.get_logic())
    1.88 +    theory_view.activate()
    1.89 +    Isabelle.session.begin_document(buffer.getName)
    1.90    }
    1.91  
    1.92 -  private def uninstall(view: View) =
    1.93 -    mapping.removeKey(view.getBuffer).get.deactivate
    1.94 +  private def uninstall(view: View)
    1.95 +  {
    1.96 +    val buffer = view.getBuffer
    1.97 +    mapping(buffer).deactivate
    1.98 +    mapping -= buffer
    1.99 +  }
   1.100  
   1.101    def switch_active(view: View) =
   1.102      if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
   1.103      else install(view)
   1.104  
   1.105 -  def prover_setup(buffer: JEditBuffer): Option[Prover_Setup] = mapping.get(buffer)
   1.106 -  def is_active (buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   1.107 +  def theory_view(buffer: JEditBuffer): Option[Theory_View] = mapping.get(buffer)
   1.108 +  def is_active(buffer: JEditBuffer) = mapping.isDefinedAt(buffer)
   1.109  
   1.110  
   1.111    /* main plugin plumbing */
   1.112 @@ -130,13 +115,14 @@
   1.113          val buffer = msg.getEditPane.getBuffer
   1.114          msg.getWhat match {
   1.115            case EditPaneUpdate.BUFFER_CHANGED =>
   1.116 -            (mapping get buffer) map (_.theory_view.activate)
   1.117 +            theory_view(buffer)map(_.activate)
   1.118            case EditPaneUpdate.BUFFER_CHANGING =>
   1.119              if (buffer != null)
   1.120 -              (mapping get buffer) map (_.theory_view.deactivate)
   1.121 +              theory_view(buffer).map(_.deactivate)
   1.122            case _ =>
   1.123          }
   1.124 -      case msg: PropertiesChanged => properties_changed.event(())
   1.125 +      case msg: PropertiesChanged =>
   1.126 +        Isabelle.session.global_settings.event(())
   1.127        case _ =>
   1.128      }
   1.129    }
   1.130 @@ -146,11 +132,13 @@
   1.131      Isabelle.plugin = this
   1.132      Isabelle.system = new Isabelle_System
   1.133      Isabelle.system.install_fonts()
   1.134 +    Isabelle.session = new Session(Isabelle.system)  // FIXME dialog!?
   1.135    }
   1.136  
   1.137    override def stop()
   1.138    {
   1.139 -    // TODO: proper cleanup
   1.140 +    Isabelle.session.stop()  // FIXME dialog!?
   1.141 +    Isabelle.session = null
   1.142      Isabelle.system = null
   1.143      Isabelle.plugin = null
   1.144    }