# HG changeset patch
# User wenzelm
# Date 1260137354 -3600
# Node ID 610e411384866df4e23d4f6d824de2f2e01323f5
# Parent  cbeeef3aebb39c67b84557d261f8618e37a5a7ab
output_syms: permissive treatment of control symbols, cf. Scala version;

diff -r cbeeef3aebb3 -r 610e41138486 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sun Dec 06 23:08:43 2009 +0100
+++ b/src/Pure/Thy/html.ML	Sun Dec 06 23:09:14 2009 +0100
@@ -58,7 +58,8 @@
   val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
 
   val html_syms = Symtab.make
-   [("\n", (0, "<br/>")),
+   [("", (0, "")),
+    ("\n", (0, "<br/>")),
     ("'", (1, "&#39;")),
     ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
     ("\\<exclamdown>", (1, "&iexcl;")),
@@ -221,13 +222,14 @@
   val output_bold = output_markup (span "bold");
   val output_loc = output_markup (span "loc");
 
-  fun output_syms (s1 :: s2 :: ss) =
-        if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
-        else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
-        else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
-        else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
-        else output_sym s1 :: output_syms (s2 :: ss)
-    | output_syms (s :: ss) = output_sym s :: output_syms ss
+  fun output_syms (s1 :: rest) =
+        let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in
+          if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
+          else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
+          else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
+          else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
+          else output_sym s1 :: output_syms rest
+        end
     | output_syms [] = [];
 in