# HG changeset patch
# User wenzelm
# Date 1219699676 -7200
# Node ID c26e0373c24f89f37de510b4f761bd51d84a3ba1
# Parent  2cd94c30271c917b2cd55f68911f1e20bc82d147
moved new Symbol.Interpretation into plugin;

diff -r 2cd94c30271c -r c26e0373c24f lib/jedit/plugin/isabelle_plugin.scala
--- a/lib/jedit/plugin/isabelle_plugin.scala	Mon Aug 25 22:42:04 2008 +0200
+++ b/lib/jedit/plugin/isabelle_plugin.scala	Mon Aug 25 23:27:56 2008 +0200
@@ -26,13 +26,18 @@
 
 object IsabellePlugin {
 
+  /* Isabelle symbols */
+
+  val symbols = new Symbol.Interpretation
+
+  def result_content(result: IsabelleProcess.Result) =
+    XML.content(YXML.parse_failsafe(symbols.decode(result.result))).mkString("")
+
+
   /* Isabelle process */
 
   var isabelle: IsabelleProcess = null
 
-  def result_content(result: IsabelleProcess.Result) =
-    XML.content(isabelle.decode_result(result)).mkString("")
-
 
   /* unique ids */
 
@@ -149,6 +154,7 @@
 
   }
 
+
   override def stop = {
     isabelle.kill
     consumer_thread.join
diff -r 2cd94c30271c -r c26e0373c24f src/Pure/Tools/isabelle_process.scala
--- a/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 22:42:04 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.scala	Mon Aug 25 23:27:56 2008 +0200
@@ -84,12 +84,6 @@
   def session() = the_session
 
 
-  /* symbols */
-
-  val symbols = new Symbol.Interpretation
-  def decode_result(result: Result) = YXML.parse_failsafe(symbols.decode(result.result))
-
-
   /* results */
 
   private val results = new LinkedBlockingQueue[Result]