1.1 --- a/src/Pure/Thy/html.ML	Sun Jan 09 12:56:00 2011 +0100
     1.2 +++ b/src/Pure/Thy/html.ML	Sun Jan 09 13:58:31 2011 +0100
     1.3 @@ -221,22 +221,20 @@
     1.4    val output_bold = output_markup (span "bold");
     1.5    val output_loc = output_markup (span "loc");
     1.6  
     1.7 -  fun output_syms (s1 :: rest) =
     1.8 -        let val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss)) in
     1.9 -          if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then output_sub s1 s2 :: output_syms ss
    1.10 -          else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then output_sup s1 s2 :: output_syms ss
    1.11 -          else if s1 = "\\<^bold>" then output_bold s1 s2 :: output_syms ss
    1.12 -          else if s1 = "\\<^loc>" then output_loc s1 s2 :: output_syms ss
    1.13 -          else output_sym s1 :: output_syms rest
    1.14 -        end
    1.15 -    | output_syms [] = [];
    1.16 +  fun output_syms [] (result, width) = (implode (rev result), width)
    1.17 +    | output_syms (s1 :: rest) (result, width) =
    1.18 +        let
    1.19 +          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
    1.20 +          val ((w, s), r) =
    1.21 +            if s1 = "\\<^sub>" orelse s1 = "\\<^isub>" then (output_sub s1 s2, ss)
    1.22 +            else if s1 = "\\<^sup>" orelse s1 = "\\<^isup>" then (output_sup s1 s2, ss)
    1.23 +            else if s1 = "\\<^bold>" then (output_bold s1 s2, ss)
    1.24 +            else if s1 = "\\<^loc>" then (output_loc s1 s2, ss)
    1.25 +            else (output_sym s1, rest);
    1.26 +        in output_syms r (s :: result, width + w) end;
    1.27  in
    1.28  
    1.29 -fun output_width str =
    1.30 -  let val (syms, width) =
    1.31 -    fold_map (fn (w, s) => fn width => (s, w + width)) (output_syms (Symbol.explode str)) 0
    1.32 -  in (implode syms, width) end;
    1.33 -
    1.34 +fun output_width str = output_syms (Symbol.explode str) ([], 0);
    1.35  val output = #1 o output_width;
    1.36  
    1.37  val _ = Output.add_mode htmlN output_width Symbol.encode_raw;