equal
deleted
inserted
replaced
110 def cache_props(x: List[(String, String)]): List[(String, String)] = |
110 def cache_props(x: List[(String, String)]): List[(String, String)] = |
111 if (x.isEmpty) x |
111 if (x.isEmpty) x |
112 else |
112 else |
113 lookup(x) match { |
113 lookup(x) match { |
114 case Some(y) => y |
114 case Some(y) => y |
115 case None => store(x.map(p => (cache_string(p._1), cache_string(p._2)))) |
115 case None => store(x.map(p => (cache_string(p._1).intern, cache_string(p._2)))) |
116 } |
116 } |
117 def cache_markup(x: Markup): Markup = |
117 def cache_markup(x: Markup): Markup = |
118 lookup(x) match { |
118 lookup(x) match { |
119 case Some(y) => y |
119 case Some(y) => y |
120 case None => |
120 case None => |