cache results;
authorwenzelm
Fri, 18 Dec 2009 21:46:29 +0100
changeset 34795 c97335b7e8c3
parent 34794 a4a457e393a4
child 34796 e65352f12421
cache results;
src/Tools/jEdit/src/proofdocument/session.scala
--- 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)