# HG changeset patch
# User wenzelm
# Date 1260030647 -3600
# Node ID 041dc6d8d344aab73538c0eb0514c176f8414d48
# Parent  1d33e85a3fa93991520785a3e1e58d7e3b80c571
output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
output_width: uniform mapping -- avoid obscure fastpath optimization;

diff -r 1d33e85a3fa9 -r 041dc6d8d344 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML	Sat Dec 05 16:39:49 2009 +0100
+++ b/src/Pure/Thy/html.ML	Sat Dec 05 17:30:47 2009 +0100
@@ -58,7 +58,8 @@
   val hidden = XML.text #> (span Markup.hiddenN |-> enclose);
 
   val html_syms = Symtab.make
-   [("'", (1, "&#39;")),
+   [("\n", (0, "<br/>")),
+    ("'", (1, "&#39;")),
     ("\\<spacespace>", (2, "&nbsp;&nbsp;")),
     ("\\<exclamdown>", (1, "&iexcl;")),
     ("\\<cent>", (1, "&cent;")),
@@ -231,12 +232,9 @@
 in
 
 fun output_width str =
-  if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
-  then Output.default_output str
-  else
-    let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
-      (output_syms (Symbol.explode str)) 0
-    in (implode syms, width) end;
+  let val (syms, width) =
+    fold_map (fn (w, s) => fn width => (s, w + width)) (output_syms (Symbol.explode str)) 0
+  in (implode syms, width) end;
 
 val output = #1 o output_width;