# HG changeset patch
# User immler@in.tum.de
# Date 1231607414 -3600
# Node ID b510b7d88de2fdd73bb015f93c5483b9a6c83b44
# Parent  fefbd0421e4ec11706c8eb15f85e8bed84b80975
changed install/uninstall prover on view to private

diff -r fefbd0421e4e -r b510b7d88de2 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sat Jan 10 17:59:23 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sat Jan 10 18:10:14 2009 +0100
@@ -73,33 +73,23 @@
 
   private val mapping = new HashMap[JEditBuffer, ProverSetup]
 
-  def install(view: View) {
+  private 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")
-    }
+    val prover_setup = new ProverSetup(buffer)
+    mapping.update(buffer, prover_setup)
+    prover_setup.activate(view)
   }
 
-  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
-    }
-  }
+  private def uninstall(view: View) =
+    mapping.removeKey(view.getBuffer).get.deactivate
+
+  def switch_active (view : View) =
+    if (mapping.isDefinedAt(view.getBuffer)) uninstall(view)
+    else install(view)
 
   def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
   def is_active (buffer : JEditBuffer) = mapping.isDefinedAt(buffer)
-  def switch_active (view : View) = mapping.get(view.getBuffer) match {
-    case None => install(view)
-    case _ => uninstall(view)}
-
+  
   
   // main plugin plumbing