# HG changeset patch
# User wenzelm
# Date 1233081704 -3600
# Node ID 4bd6766627925a1c56c576e4b3ae1fd313a93a8d
# Parent  7d0726f19d0423116dcca6f21b9e25d6d0856de5
eliminated Prover.start -- part of main constructor;

diff -r 7d0726f19d04 -r 4bd676662792 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- 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
diff -r 7d0726f19d04 -r 4bd676662792 src/Tools/jEdit/src/prover/Prover.scala
--- 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))