--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jan 27 19:27:59 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala Tue Jan 27 19:41:44 2009 +0100
@@ -22,7 +22,7 @@
class ProverSetup(buffer: JEditBuffer)
{
- val prover = new Prover(Isabelle.system)
+ var prover: Prover = null
var theory_view: TheoryView = null
val state_update = new EventBus[Command]
@@ -34,7 +34,7 @@
val output_text_view = new JTextArea
def activate(view: View) {
- prover.start(Isabelle.default_logic)
+ prover = new Prover(Isabelle.system, Isabelle.default_logic)
val buffer = view.getBuffer
val dir = buffer.getDirectory
--- a/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 27 19:27:59 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala Tue Jan 27 19:41:44 2009 +0100
@@ -19,8 +19,21 @@
import isabelle.IsarDocument
-class Prover(isabelle_system: IsabelleSystem)
+class Prover(isabelle_system: IsabelleSystem, logic: String)
{
+ /* prover process */
+
+ private var process: Isar = null
+
+ {
+ val results = new EventBus[IsabelleProcess.Result] + handle_result
+ results.logger = Log.log(Log.ERROR, null, _)
+ process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
+ }
+
+ def stop() { process.kill }
+
+
/* outer syntax keywords */
val decl_info = new EventBus[(String, String)]
@@ -56,8 +69,6 @@
/* event handling */
- private var process: Isar = null
-
private val states = new mutable.HashMap[IsarDocument.State_ID, Command]
private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
private val document0 = Isabelle.plugin.id()
@@ -166,17 +177,6 @@
}
}
-
- def start(logic: String) {
- val results = new EventBus[IsabelleProcess.Result] + handle_result
- results.logger = Log.log(Log.ERROR, null, _)
- process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
- }
-
- def stop() {
- process.kill
- }
-
def set_document(text: Text, path: String) {
this.document = new ProofDocument(text, this)
process.ML("ThyLoad.add_path " + IsabelleSyntax.encode_string(path))