1.1 --- a/src/Pure/General/xml.scala Sun Jul 10 23:46:05 2011 +0200
1.2 +++ b/src/Pure/General/xml.scala Mon Jul 11 10:27:50 2011 +0200
1.3 @@ -81,7 +81,7 @@
1.4
1.5 /* pipe-lined cache for partial sharing */
1.6
1.7 - class Cache(initial_size: Int)
1.8 + class Cache(initial_size: Int = 131071, max_string: Int = 100)
1.9 {
1.10 private val cache_actor = actor
1.11 {
1.12 @@ -108,7 +108,9 @@
1.13 def cache_string(x: String): String =
1.14 lookup(x) match {
1.15 case Some(y) => y
1.16 - case None => store(trim_bytes(x))
1.17 + case None =>
1.18 + val z = trim_bytes(x)
1.19 + if (z.length > max_string) z else store(z)
1.20 }
1.21 def cache_props(x: List[(String, String)]): List[(String, String)] =
1.22 if (x.isEmpty) x
2.1 --- a/src/Pure/System/isabelle_process.scala Sun Jul 10 23:46:05 2011 +0200
2.2 +++ b/src/Pure/System/isabelle_process.scala Mon Jul 11 10:27:50 2011 +0200
2.3 @@ -90,7 +90,7 @@
2.4 receiver ! new Result(XML.Elem(Markup(Markup.SYSTEM, Nil), List(XML.Text(text))))
2.5 }
2.6
2.7 - private val xml_cache = new XML.Cache(131071)
2.8 + private val xml_cache = new XML.Cache()
2.9
2.10 private def put_result(kind: String, props: List[(String, String)], body: XML.Body)
2.11 {