# HG changeset patch
# User wenzelm
# Date 1310372870 -7200
# Node ID 562e35bc351eef52294e66de537bf412bf735d96
# Parent  2c7e1565b4a3af9345e53715651a7f6065ca8959
tuned XML.Cache parameters;

diff -r 2c7e1565b4a3 -r 562e35bc351e src/Pure/General/xml.scala
--- a/src/Pure/General/xml.scala	Sun Jul 10 23:46:05 2011 +0200
+++ b/src/Pure/General/xml.scala	Mon Jul 11 10:27:50 2011 +0200
@@ -81,7 +81,7 @@
 
   /* pipe-lined cache for partial sharing */
 
-  class Cache(initial_size: Int)
+  class Cache(initial_size: Int = 131071, max_string: Int = 100)
   {
     private val cache_actor = actor
     {
@@ -108,7 +108,9 @@
       def cache_string(x: String): String =
         lookup(x) match {
           case Some(y) => y
-          case None => store(trim_bytes(x))
+          case None =>
+            val z = trim_bytes(x)
+            if (z.length > max_string) z else store(z)
         }
       def cache_props(x: List[(String, String)]): List[(String, String)] =
         if (x.isEmpty) x
diff -r 2c7e1565b4a3 -r 562e35bc351e src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Sun Jul 10 23:46:05 2011 +0200
+++ b/src/Pure/System/isabelle_process.scala	Mon Jul 11 10:27:50 2011 +0200
@@ -90,7 +90,7 @@
     receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
   }
 
-  private val xml_cache = new XML.Cache(131071)
+  private val xml_cache = new XML.Cache()
 
   private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
   {