equal
deleted
inserted
replaced
78 } |
78 } |
79 def add(elem: XML.Tree) { |
79 def add(elem: XML.Tree) { |
80 flush() |
80 flush() |
81 ts += elem |
81 ts += elem |
82 } |
82 } |
83 val syms = Symbol.iterator_string(txt) |
83 val syms = Symbol.iterator(txt) |
84 while (syms.hasNext) { |
84 while (syms.hasNext) { |
85 val s1 = syms.next |
85 val s1 = syms.next |
86 def s2() = if (syms.hasNext) syms.next else "" |
86 def s2() = if (syms.hasNext) syms.next else "" |
87 if (s1 == "\n") add(XML.elem(BR)) |
87 if (s1 == "\n") add(XML.elem(BR)) |
88 else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME |
88 else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME |