# HG changeset patch
# User immler@in.tum.de
# Date 1229682306 -3600
# Node ID cc5b9f02fbea35cdb9a98546f3d9afe1c8303d4d
# Parent  f81cd75ae3312dc2942b6101e8ea0db7a03453d2
ability to deactivate buffers

diff -r f81cd75ae331 -r cc5b9f02fbea src/Tools/jEdit/plugin/actions.xml
--- a/src/Tools/jEdit/plugin/actions.xml	Thu Dec 18 01:10:20 2008 +0100
+++ b/src/Tools/jEdit/plugin/actions.xml	Fri Dec 19 11:25:06 2008 +0100
@@ -16,7 +16,7 @@
 	</ACTION>
 	<ACTION NAME="Isabelle.activate">
 		<CODE>
-			isabelle.jedit.Plugin$.MODULE$.plugin().install(view);
+			isabelle.jedit.Plugin$.MODULE$.plugin().switch_active(view);
 		</CODE>
 		<IS_SELECTED>
 			return isabelle.jedit.Plugin$.MODULE$.plugin().is_active(view.getBuffer());
diff -r f81cd75ae331 -r cc5b9f02fbea src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Thu Dec 18 01:10:20 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Fri Dec 19 11:25:06 2008 +0100
@@ -63,6 +63,9 @@
 
   def prover_setup (buffer : JEditBuffer) : Option[ProverSetup] = mapping.get(buffer)
   def is_active (buffer : JEditBuffer) = mapping.get(buffer) match { case None => false case _ => true}
+  def switch_active (view : View) = mapping.get(view.getBuffer) match {
+    case None => install(view)
+    case _ => uninstall(view)}
   
   override def handleMessage(msg : EBMessage) = msg match {
     case epu : EditPaneUpdate => epu.getWhat() match {
diff -r f81cd75ae331 -r cc5b9f02fbea src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Thu Dec 18 01:10:20 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Fri Dec 19 11:25:06 2008 +0100
@@ -81,7 +81,8 @@
   }
 
   def deactivate {
-    //TODO: clean up!
+    theory_view.deactivate
+    prover.stop
   }
 
 }
diff -r f81cd75ae331 -r cc5b9f02fbea src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Thu Dec 18 01:10:20 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Fri Dec 19 11:25:06 2008 +0100
@@ -37,7 +37,7 @@
   def fireChange(c : Command) =
     inUIThread(() => commandInfo.fire(new CommandChangeInfo(c)))
 
-  var workerThread = new Thread("isabelle.Prover: worker") {
+  val worker_thread = new Thread("isabelle.Prover: worker") {
     override def run() : Unit = {
       while (true) {
         val r = process.get_result
@@ -114,9 +114,7 @@
   }
   
   def handleResult(st : Command, r : Result, tree : XML.Tree) {
-    //TODO: this is just for testing
-    allInfo.fire(r)
-    
+
     r.kind match {
       case IsabelleProcess.Kind.ERROR => 
         if (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE)
@@ -149,7 +147,7 @@
     if (logic != null)
       _logic = logic
     process = new IsabelleProcess("-m", "xsymbols", _logic)
-    workerThread.start
+    worker_thread.start
   }
 
   def stop() {
@@ -200,6 +198,7 @@
   
   def remove(cmd : Command) {
     cmd.phase = Phase.REMOVE
-    process.output_sync("Isar.remove " + encode_string(cmd.idString))
+      process.output_sync("Isar.remove " + encode_string(cmd.idString))
+
   }
 }
\ No newline at end of file