equal
deleted
inserted
replaced
90 case Some((s, rest)) => { state = get_nexts(rest); s } |
90 case Some((s, rest)) => { state = get_nexts(rest); s } |
91 case None => throw new NoSuchElementException("next on empty iterator") |
91 case None => throw new NoSuchElementException("next on empty iterator") |
92 } |
92 } |
93 } |
93 } |
94 |
94 |
95 def content_length(tree: XML.Tree): Int = |
|
96 tree match { |
|
97 case Elem(_, _, body) => (0 /: body)(_ + content_length(_)) |
|
98 case Text(s) => s.length |
|
99 } |
|
100 |
|
101 |
95 |
102 /* cache for partial sharing -- NOT THREAD SAFE */ |
96 /* cache for partial sharing -- NOT THREAD SAFE */ |
103 |
97 |
104 class Cache(initial_size: Int) |
98 class Cache(initial_size: Int) |
105 { |
99 { |