equal
deleted
inserted
replaced
55 def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) |
55 def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt))) |
56 def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt))) |
56 def bold(txt: String): XML.Elem = span("bold", List(XML.Text(txt))) |
57 |
57 |
58 def spans(input: XML.Tree, original_data: Boolean = false): XML.Body = |
58 def spans(input: XML.Tree, original_data: Boolean = false): XML.Body = |
59 { |
59 { |
60 val symbols = Isabelle_System.symbols |
|
61 |
|
62 def html_spans(tree: XML.Tree): XML.Body = |
60 def html_spans(tree: XML.Tree): XML.Body = |
63 tree match { |
61 tree match { |
64 case XML.Elem(m @ Markup(name, props), ts) => |
62 case XML.Elem(m @ Markup(name, props), ts) => |
65 val span_class = |
63 val span_class = |
66 m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name } |
64 m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name } |
83 val syms = Symbol.iterator(txt) |
81 val syms = Symbol.iterator(txt) |
84 while (syms.hasNext) { |
82 while (syms.hasNext) { |
85 val s1 = syms.next |
83 val s1 = syms.next |
86 def s2() = if (syms.hasNext) syms.next else "" |
84 def s2() = if (syms.hasNext) syms.next else "" |
87 if (s1 == "\n") add(XML.elem(BR)) |
85 if (s1 == "\n") add(XML.elem(BR)) |
88 else if (s1 == symbols.bsub_decoded) t ++= s1 // FIXME |
86 else if (Symbol.is_bsub_decoded(s1)) t ++= s1 // FIXME |
89 else if (s1 == symbols.esub_decoded) t ++= s1 // FIXME |
87 else if (Symbol.is_esub_decoded(s1)) t ++= s1 // FIXME |
90 else if (s1 == symbols.bsup_decoded) t ++= s1 // FIXME |
88 else if (Symbol.is_bsup_decoded(s1)) t ++= s1 // FIXME |
91 else if (s1 == symbols.esup_decoded) t ++= s1 // FIXME |
89 else if (Symbol.is_esup_decoded(s1)) t ++= s1 // FIXME |
92 else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) } |
90 else if (Symbol.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) } |
93 else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) } |
91 else if (Symbol.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) } |
94 else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) } |
92 else if (Symbol.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) } |
95 else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) } |
93 else if (Symbol.fonts.isDefinedAt(s1)) { add(user_font(Symbol.fonts(s1), s1)) } |
96 else t ++= s1 |
94 else t ++= s1 |
97 } |
95 } |
98 flush() |
96 flush() |
99 ts.toList |
97 ts.toList |
100 } |
98 } |