equal
deleted
inserted
replaced
100 { |
100 { |
101 table.put(x, new WeakReference[Any](x)) |
101 table.put(x, new WeakReference[Any](x)) |
102 x |
102 x |
103 } |
103 } |
104 |
104 |
|
105 def trim_bytes(s: String): String = new String(s.toCharArray) |
|
106 |
105 def cache_string(x: String): String = |
107 def cache_string(x: String): String = |
106 lookup(x) match { |
108 lookup(x) match { |
107 case Some(y) => y |
109 case Some(y) => y |
108 case None => store(new String(x.toCharArray)) // trim string value |
110 case None => store(trim_bytes(x)) |
109 } |
111 } |
110 def cache_props(x: List[(String, String)]): List[(String, String)] = |
112 def cache_props(x: List[(String, String)]): List[(String, String)] = |
111 if (x.isEmpty) x |
113 if (x.isEmpty) x |
112 else |
114 else |
113 lookup(x) match { |
115 lookup(x) match { |
114 case Some(y) => y |
116 case Some(y) => y |
115 case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2)))) |
117 case None => store(x.map(p => (trim_bytes(p._1).intern, cache_string(p._2)))) |
116 } |
118 } |
117 def cache_markup(x: Markup): Markup = |
119 def cache_markup(x: Markup): Markup = |
118 lookup(x) match { |
120 lookup(x) match { |
119 case Some(y) => y |
121 case Some(y) => y |
120 case None => |
122 case None => |