output linefeed as </br> -- workaround problem with <pre> in Lobo Browser 0.98.4;
output_width: uniform mapping -- avoid obscure fastpath optimization;
--- 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, "'")),
+ [("\n", (0, "<br/>")),
+ ("'", (1, "'")),
("\\<spacespace>", (2, " ")),
("\\<exclamdown>", (1, "¡")),
("\\<cent>", (1, "¢")),
@@ -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;