use Symbol.Interpretation from IsabelleSystem instance;
authorwenzelm
Tue, 20 Jan 2009 20:05:21 +0100
changeset 34490 820d0675e7b5
parent 34489 7b7ccf0ff629
child 34491 20e9d420dbbb
use Symbol.Interpretation from IsabelleSystem instance;
src/Tools/jEdit/src/jedit/ProverSetup.scala
src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 20 18:23:40 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Tue Jan 20 20:05:21 2009 +0100
@@ -22,7 +22,7 @@
 
 class ProverSetup(buffer: JEditBuffer)
 {
-  val prover = new Prover(Isabelle.system, Isabelle.symbols)
+  val prover = new Prover(Isabelle.system)
   var theory_view: TheoryView = null
 
   val state_update = new EventBus[Command]
--- a/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 20 18:23:40 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Tue Jan 20 20:05:21 2009 +0100
@@ -18,7 +18,7 @@
 import isabelle.IsarDocument
 
 
-class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation)
+class Prover(isabelle_system: IsabelleSystem)
 {
   private var _logic = isabelle_system.getenv_strict("ISABELLE_LOGIC")
   private var process: Isar = null
@@ -196,7 +196,7 @@
     cmd.status = Command.Status.UNPROCESSED
     commands.put(cmd.id, cmd)
 
-    val content = isabelle_symbols.encode(document.getContent(cmd))
+    val content = isabelle_system.symbols.encode(document.getContent(cmd))
     process.create_command(cmd.id, content)
     process.insert_command(if (cmd.prev == null) "" else cmd.prev.id, cmd.id)
   }