# HG changeset patch
# User wenzelm
# Date 1233073375 -3600
# Node ID f97b764f956f9bb0efd5840c95de198808a40b19
# Parent  184fda8cce0494fdc6bdbb8efc81e309cb8c8043
Prover.start: determine logic in one place;

diff -r 184fda8cce04 -r f97b764f956f src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 27 16:16:55 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 27 17:22:55 2009 +0100
@@ -34,7 +34,9 @@
   val output_text_view = new JTextArea
 
   def activate(view: View) {
-    prover.start(Isabelle.Property("logic"))
+    val logic = Isabelle.Property("logic")
+    prover.start(if (logic != null) logic else Isabelle.system.getenv_strict("ISABELLE_LOGIC"))
+    
     val buffer = view.getBuffer
     val dir = buffer.getDirectory
 
diff -r 184fda8cce04 -r f97b764f956f src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 16:16:55 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 27 17:22:55 2009 +0100
@@ -20,7 +20,6 @@
 
 class Prover(isabelle_system: IsabelleSystem)
 {
-  private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
   private var process: Isar = null
 
   private val commands = new mutable.HashMap[IsarDocument.Command_ID, Command]
@@ -165,13 +164,10 @@
 
 
   def start(logic: String) {
-    if (logic != null) _logic = logic
-
     val results = new EventBus[IsabelleProcess.Result]
     results += handle_result
     results.logger = Log.log(Log.ERROR, null, _)
-
-    process = new Isar(isabelle_system, results, "-m", "xsymbols", _logic)
+    process = new Isar(isabelle_system, results, "-m", "xsymbols", logic)
   }
 
   def stop() {