src/Pure/Thy/html.scala
changeset 43458 b55a273ede18
parent 43455 4b4b93672f15
child 43459 def9784a3316
--- a/src/Pure/Thy/html.scala	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
@@ -86,7 +86,6 @@
             else if (symbols.is_bold_decoded(s1)) {
               add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
             }
-            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
             else t ++= s1
           }
           flush()