# HG changeset patch
# User wenzelm
# Date 1260138327 -3600
# Node ID 30c8746074d0ea0c9305f508a2db1ece32262764
# Parent  610e411384866df4e23d4f6d824de2f2e01323f5
proper markup text for loc;

diff -r 610e41138486 -r 30c8746074d0 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Dec 06 23:09:14 2009 +0100
+++ b/src/Pure/Thy/html.scala	Sun Dec 06 23:25:27 2009 +0100
@@ -61,7 +61,7 @@
             case "\\<^sub>" | "\\<^isub>" => add(hidden(s1)); add(sub(s2))
             case "\\<^sup>" | "\\<^isup>" => add(hidden(s1)); add(sup(s2))
             case "\\<^bold>" => add(hidden(s1)); add(span("bold", List(XML.Text(s2))))
-            case "\\<^loc>" => add(hidden(s2)); add(span("loc", List(XML.Text(s2))))
+            case "\\<^loc>" => add(hidden(s1)); add(span("loc", List(XML.Text(s2))))
             case _ => t ++ s1
           }
         }