src/Pure/PIDE/xml.scala

--- a/src/Pure/PIDE/xml.scala	Wed Sep 07 22:00:41 2011 +0200
+++ b/src/Pure/PIDE/xml.scala	Wed Sep 07 23:08:04 2011 +0200
@@ -84,7 +84,8 @@
   def content(body: Body): Iterator[String] = content_stream(body).iterator
 
 
-  /* pipe-lined cache for partial sharing */
+
+  /** cache for partial sharing (weak table) **/
 
   class Cache(initial_size: Int = 131071, max_string: Int = 100)
   {