# HG changeset patch
# User wenzelm
# Date 1230387646 -3600
# Node ID f2e13329cc49bc79ebdc598ecfc5cb55b94b2fb9
# Parent  9e6d80c387e0f20afee1a2e918a3f176f8a87b30
dynamic instances Isabelle.system, Isabelle.symbols;

diff -r 9e6d80c387e0 -r f2e13329cc49 src/Tools/jEdit/src/jedit/Plugin.scala
--- a/src/Tools/jEdit/src/jedit/Plugin.scala	Sat Dec 27 15:20:02 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Sat Dec 27 15:20:46 2008 +0100
@@ -132,7 +132,7 @@
 
   override def start() {
     Isabelle.system = new IsabelleSystem
-    Isabelle.symbols = new Symbol.Interpretation(system)
+    Isabelle.symbols = new Symbol.Interpretation(Isabelle.system)
     Isabelle.plugin = this
     
     if (Isabelle.property("font-path") != null && Isabelle.property("font-size") != null)
diff -r 9e6d80c387e0 -r f2e13329cc49 src/Tools/jEdit/src/jedit/ProverSetup.scala
--- a/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sat Dec 27 15:20:02 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/ProverSetup.scala	Sat Dec 27 15:20:46 2008 +0100
@@ -23,7 +23,7 @@
 
 class ProverSetup(buffer : JEditBuffer) {
 
-  val prover = new Prover()
+  val prover = new Prover(Isabelle.system, Isabelle.symbols)
   var theory_view : TheoryView = null
   
   private var _selectedState : Command = null
diff -r 9e6d80c387e0 -r f2e13329cc49 src/Tools/jEdit/src/jedit/VFS.scala
--- a/src/Tools/jEdit/src/jedit/VFS.scala	Sat Dec 27 15:20:02 2008 +0100
+++ b/src/Tools/jEdit/src/jedit/VFS.scala	Sat Dec 27 15:20:46 2008 +0100
@@ -163,7 +163,7 @@
   
   override def _createInputStream(session: Object, path: String,
       ignoreErrors: Boolean, comp: Component) =
-    VFS.input_converter(baseVFS._createInputStream(session, cutPath(path), ignoreErrors, comp))
+    VFS.input_converter(Isabelle.system, baseVFS._createInputStream(session, cutPath(path), ignoreErrors, comp))
   
   override def _createOutputStream(session: Object, path: String, comp: Component) =
     new VFS.OutputConverter(baseVFS._createOutputStream(session, cutPath(path), comp))
diff -r 9e6d80c387e0 -r f2e13329cc49 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sat Dec 27 15:20:02 2008 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sat Dec 27 15:20:46 2008 +0100
@@ -7,28 +7,26 @@
 
 package isabelle.prover
 
-import scala.collection.mutable.{ HashMap, HashSet }
+import scala.collection.mutable.{HashMap, HashSet}
 
 import java.util.Properties
 
 import javax.swing.SwingUtilities
 
-import isabelle.proofdocument.{ ProofDocument, Text, Token }
+import isabelle.proofdocument.{ProofDocument, Text, Token}
 import isabelle.IsabelleProcess.Result
 import isabelle.YXML.parse_failsafe
-import isabelle.XML.{ Elem, Tree }
-import isabelle.Symbol.Interpretation
-import isabelle.IsabelleSyntax.{ encode_properties, encode_string }
+import isabelle.XML.{Elem, Tree}
+import isabelle.Symbol
+import isabelle.IsabelleSyntax.{encode_properties, encode_string}
 
 import isabelle.utils.EventSource
 
 import Command.Phase
 
-class Prover() {
-  val converter = new Interpretation()
-
-  private var _logic = "HOL"
-  private var process = null : IsabelleProcess
+class Prover(isabelle_system: IsabelleSystem, isabelle_symbols: Symbol.Interpretation) {
+  private var _logic = "HOL"   // FIXME avoid hardwired settings
+  private var process = null: IsabelleProcess
   private var commands = new HashMap[String, Command]
   
   val command_decls = new HashSet[String]
@@ -67,7 +65,7 @@
           )
         }
         else {
-          val tree = parse_failsafe(converter.decode(r.result))
+          val tree = parse_failsafe(isabelle_symbols.decode(r.result))
           if (st == null || (st.phase != Phase.REMOVED && st.phase != Phase.REMOVE))
           tree match {
             //handle all kinds of status messages here
@@ -155,7 +153,7 @@
   def start(logic : String) {
     if (logic != null)
       _logic = logic
-    process = new IsabelleProcess("-m", "xsymbols", _logic)
+    process = new IsabelleProcess(isabelle_system, "-m", "xsymbols", _logic)
     workerThread.start
   }
 
@@ -190,7 +188,7 @@
     props.setProperty("id", cmd.idString)
     props.setProperty("offset", Integer.toString(1))
 
-    val content = converter.encode(document.getContent(cmd))
+    val content = isabelle_symbols.encode(document.getContent(cmd))
     process.output_sync("Isar.command " 
                         + encode_properties(props)
                         + " "