# HG changeset patch
# User wenzelm
# Date 1232478321 -3600
# Node ID 820d0675e7b5fce6702f5de541aa9ff56e22c204
# Parent  7b7ccf0ff62983c10ccf0e368d00431a524aa95c
use Symbol.Interpretation from IsabelleSystem instance;

diff -r 7b7ccf0ff629 -r 820d0675e7b5 src/Tools/jEdit/src/jedit/ProverSetup.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]
diff -r 7b7ccf0ff629 -r 820d0675e7b5 src/Tools/jEdit/src/prover/Prover.scala
--- 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)
   }