--- 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());
--- 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 {
--- 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
}
}
--- 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