equal
deleted
inserted
replaced
59 case "\\<^bsup>" => t ++ s1 // FIXME |
59 case "\\<^bsup>" => t ++ s1 // FIXME |
60 case "\\<^esup>" => t ++ s1 // FIXME |
60 case "\\<^esup>" => t ++ s1 // FIXME |
61 case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2)) |
61 case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2)) |
62 case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2)) |
62 case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2)) |
63 case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2)))) |
63 case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2)))) |
64 case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2)))) |
64 case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2)))) |
65 case _ => t ++ s1 |
65 case _ => t ++ s1 |
66 } |
66 } |
67 } |
67 } |
68 flush() |
68 flush() |
69 ts.toList |
69 ts.toList |