--- a/src/Tools/jEdit/src/proofdocument/session.scala Fri Dec 18 15:00:08 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala Fri Dec 18 21:46:29 2009 +0100
@@ -32,6 +32,7 @@
private var prover_ready = false
private val session_actor = actor {
+ val xml_cache = new XML.Cache(131071)
loop {
react {
case Start(args) =>
@@ -49,7 +50,7 @@
handle_change(change)
case result: Isabelle_Process.Result =>
- handle_result(result)
+ handle_result(result.cache(xml_cache))
case bad if prover_ready =>
System.err.println("session_actor: ignoring bad message " + bad)