equal
deleted
inserted
replaced
162 current_body = body |
162 current_body = body |
163 val html_body = |
163 val html_body = |
164 current_body.flatMap(div => |
164 current_body.flatMap(div => |
165 Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) |
165 Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics)) |
166 .map(t => |
166 .map(t => |
167 XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Markup.MESSAGE))), HTML.spans(t, true)))) |
167 XML.Elem(Markup(HTML.PRE, List((HTML.CLASS, Isabelle_Markup.MESSAGE))), |
|
168 HTML.spans(t, true)))) |
168 val doc = |
169 val doc = |
169 builder.parse( |
170 builder.parse( |
170 new InputSourceImpl( |
171 new InputSourceImpl( |
171 new StringReader(template(current_font_family, current_font_size)), "http://localhost")) |
172 new StringReader(template(current_font_family, current_font_size)), "http://localhost")) |
172 doc.removeChild(doc.getLastChild()) |
173 doc.removeChild(doc.getLastChild()) |