src/Tools/jEdit/src/jedit/Plugin.scala
changeset 34406 f81cd75ae331
parent 34337 5d5b69f2956b
child 34407 aad6834ba380
child 34460 cc5b9f02fbea
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Dec 15 16:34:19 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Dec 18 01:10:20 2008 +0100
@@ -2,7 +2,7 @@
 
 import java.awt.Font
 import java.io.{ FileInputStream, IOException }
-
+import javax.swing.JScrollPane
 
 import isabelle.utils.EventSource
 
@@ -10,7 +10,11 @@
 
 import isabelle.IsabelleSystem
 
-import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, View }
+import scala.collection.mutable.HashMap
+
+import org.gjt.sp.jedit.{ jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View }
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.JEditTextArea
 import org.gjt.sp.jedit.msg.{ EditPaneUpdate, PropertiesChanged }
 
 object Plugin {
@@ -23,45 +27,68 @@
     jEdit.setProperty(OPTION_PREFIX + name, value)
   
   var plugin : Plugin = null
+  def prover(buffer : JEditBuffer) = plugin.prover_setup(buffer).get.prover
+  def prover_setup(buffer : JEditBuffer) = plugin.prover_setup(buffer).get
+
 }
 
 class Plugin extends EBPlugin {
   import Plugin._
-  
-  val prover = new Prover()
-  var theoryView : TheoryView = null
-  
-  var viewFont : Font = null 
+
+  private val mapping = new HashMap[JEditBuffer, ProverSetup]
+
+  var viewFont : Font = null
   val viewFontChanged = new EventSource[Font]
-  
-  private var _selectedState : Command = null
-  
-  val stateUpdate = new EventSource[Command]
-  
-  def selectedState = _selectedState
-  def selectedState_=(newState : Command) {
-    _selectedState = newState
-    stateUpdate fire newState
+
+  def install(view : View) {
+    val buffer = view.getBuffer
+    mapping.get(buffer) match{
+      case None =>{
+          val prover_setup = new ProverSetup(buffer)
+          mapping.update(buffer, prover_setup)
+          prover_setup.activate(view)
+      }
+      case _ => System.err.println("Already installed plugin on Buffer")
+    }
   }
-  
-  def activate(view : View) {
-    val logic = property("logic")
-    theoryView = new TheoryView(prover, view.getBuffer())
-    prover.start(if (logic == null) logic else "HOL")
-    val dir = view.getBuffer().getDirectory()
-    prover.setDocument(theoryView, 
-                       if (dir.startsWith(VFS_PREFIX)) dir.substring(VFS_PREFIX.length) else dir)
-    TheoryView.activateTextArea(view.getTextArea())
+
+  def uninstall(view : View) {
+    val buffer = view.getBuffer
+    mapping.removeKey(buffer) match{
+      case None => System.err.println("No Plugin installed on this Buffer")
+      case Some(proversetup) =>
+        proversetup.deactivate
+    }
   }
+
+  def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
+  def is_active (buffer : JEditBuffer) = mapping.get(buffer) match { case None => false case _ => true}
   
   override def handleMessage(msg : EBMessage) = msg match {
     case epu : EditPaneUpdate => epu.getWhat() match {
       case EditPaneUpdate.BUFFER_CHANGED =>
-        TheoryView.activateTextArea(epu.getEditPane().getTextArea())
-
+        mapping get epu.getEditPane.getBuffer match {
+          //only activate 'isabelle'-buffers!
+          case None =>
+          case Some(prover_setup) => 
+            prover_setup.theory_view.activate
+            val dockable = epu.getEditPane.getView.getDockableWindowManager.getDockable("Isabelle_output")
+            if(dockable != null) {
+              val output_dockable = dockable.asInstanceOf[OutputDockable]
+              if(output_dockable.getComponent(0) != prover_setup.output_text_view ) {
+                output_dockable.asInstanceOf[OutputDockable].removeAll
+                output_dockable.asInstanceOf[OutputDockable].add(new JScrollPane(prover_setup.output_text_view))
+                output_dockable.revalidate
+              }
+            }
+        }
       case EditPaneUpdate.BUFFER_CHANGING =>
-        TheoryView.deactivateTextArea(epu.getEditPane().getTextArea())
-
+        val buffer = epu.getEditPane.getBuffer
+        if(buffer != null) mapping get buffer match {
+          //only deactivate 'isabelle'-buffers!
+          case None =>
+          case Some(prover_setup) => prover_setup.theory_view.deactivate
+        }
       case _ =>
     }
       
@@ -73,7 +100,7 @@
       val fontStream = new FileInputStream(path)
       val font = Font.createFont(Font.TRUETYPE_FONT, fontStream)
       viewFont = font.deriveFont(Font.PLAIN, size)
-      
+
       viewFontChanged.fire(viewFont)
     }
     catch {
@@ -83,7 +110,7 @@
   
   override def start() {
     plugin = this
-
+    
     if (property("font-path") != null && property("font-size") != null)
       try {
         setFont(property("font-path"), property("font-size").toFloat)