proper markup text for loc;
authorwenzelm
Sun Dec 06 23:25:27 2009 +0100 (2009-12-06 ago)
changeset 3400430c8746074d0
parent 34003 610e41138486
child 34005 ada5098506af
proper markup text for loc;
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Thy/html.scala	Sun Dec 06 23:09:14 2009 +0100
     1.2 +++ b/src/Pure/Thy/html.scala	Sun Dec 06 23:25:27 2009 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4              case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2))
     1.5              case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2))
     1.6              case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2))))
     1.7 -            case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2))))
     1.8 +            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2))))
     1.9              case _ => t ++ s1
    1.10            }
    1.11          }