src/Tools/jEdit/src/html_panel.scala
changeset 43455 4b4b93672f15
parent 43442 e1fff67b23ac
child 43520 cec9b95fa35d
     1.1 --- a/src/Tools/jEdit/src/html_panel.scala	Sun Jun 19 00:03:44 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/html_panel.scala	Sun Jun 19 14:11:06 2011 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4            Pretty.formatted(List(div), current_margin, Pretty.font_metric(current_font_metrics))
     1.5              .map(t =>
     1.6                XML.Elem(Markup(HTML.PRE, List((Markup.CLASS, Markup.MESSAGE))),
     1.7 -                HTML.spans(t, true))))
     1.8 +                HTML.spans(system.symbols, t, true))))
     1.9        val doc =
    1.10          builder.parse(
    1.11            new InputSourceImpl(