# HG changeset patch
# User wenzelm
# Date 1261169189 -3600
# Node ID c97335b7e8c3c4a3f57e89a29ea95c5be9907024
# Parent  a4a457e393a4b5c9d73b8bcaf024ea443d96beb9
cache results;

diff -r a4a457e393a4 -r c97335b7e8c3 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)