src/Tools/WWW_Find/html_unicode.ML
author wenzelm
Thu May 27 18:10:37 2010 +0200 (2010-05-27)
changeset 37146 f652333bbf8e
parent 33817 f6a4da31f2f1
child 37744 3daaf23b9ab4
permissions -rw-r--r--
renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
     1 (*  Title:      html_unicode.ML
     2     Author:     Timothy Bourke, NICTA
     3                 Based on Pure/Thy/html.ML
     4                 by Markus Wenzel and Stefan Berghofer, TU Muenchen
     5 
     6 HTML presentation elements that use unicode code points.
     7 *)
     8 
     9 signature HTML_UNICODE =
    10 sig
    11   val print_mode: ('a -> 'b) -> 'a -> 'b
    12 end;
    13 
    14 structure HTML_Unicode: HTML_UNICODE =
    15 struct
    16 
    17 (** HTML print modes **)
    18 
    19 (* mode *)
    20 
    21 val htmlunicodeN = "HTMLUnicode";
    22 fun print_mode f x = Print_Mode.with_modes [htmlunicodeN, Symbol.xsymbolsN] f x;
    23 
    24 (* symbol output *)
    25 
    26 local
    27   val sym_width_lookup = Symtab.make
    28    [("\<spacespace>", 2),
    29     ("\<Longleftarrow>", 2),
    30     ("\<longleftarrow>", 2),
    31     ("\<Longrightarrow>", 2),
    32     ("\<longrightarrow>", 2),
    33     ("\<longleftrightarrow>", 2),
    34     ("\<^bsub>", 0),
    35     ("\<^esub>", 0),
    36     ("\<^bsup>", 0),
    37     ("\<^esup>", 0)];
    38 
    39   fun sym_width s =
    40     (case Symtab.lookup sym_width_lookup s of
    41        NONE => 1
    42      | SOME w => w);
    43 
    44   fun output_sym s =
    45     if Symbol.is_raw s then (1, Symbol.decode_raw s)
    46     else
    47       (case UnicodeSymbols.symbol_to_unicode s of
    48          SOME x => (sym_width s, "&#" ^ Int.toString x ^ ";") (* numeric entities *)
    49          (* SOME x => (sym_width s, UnicodeSymbols.utf8 [x])     (* utf-8 *) *)
    50        | NONE => (size s, XML.text s));
    51 
    52   fun output_sub s = apsnd (enclose "<sub>" "</sub>") (output_sym s);
    53   fun output_sup s = apsnd (enclose "<sup>" "</sup>") (output_sym s);
    54   fun output_loc s = apsnd (enclose "<span class=\"loc\">" "</span>") (output_sym s);
    55 
    56   fun output_syms ("\<^sub>" :: s :: ss) = output_sub s :: output_syms ss
    57     | output_syms ("\<^isub>" :: s :: ss) = output_sub s :: output_syms ss
    58     | output_syms ("\<^sup>" :: s :: ss) = output_sup s :: output_syms ss
    59     | output_syms ("\<^isup>" :: s :: ss) = output_sup s :: output_syms ss
    60     | output_syms ("\<^loc>" :: s :: ss) = output_loc s :: output_syms ss
    61     | output_syms (s :: ss) = output_sym s :: output_syms ss
    62     | output_syms [] = [];
    63 
    64   fun output_width str =
    65     if not (exists_string (fn s => s = "\\" orelse s = "<" orelse s = ">" orelse s = "&") str)
    66     then Output.default_output str
    67     else
    68       let val (syms, width) = fold_map (fn (w, s) => fn width => (s, w + width))
    69         (output_syms (Symbol.explode str)) 0
    70       in (implode syms, width) end;
    71 in
    72 
    73 val output = #1 o output_width;
    74 
    75 val _ = Output.add_mode htmlunicodeN output_width Symbol.encode_raw;
    76 
    77 end;
    78 
    79 (* common markup *)
    80 
    81 fun span s = ("<span class=" ^ quote (XML.text s) ^ ">", "</span>");
    82 
    83 val _ = Markup.add_mode htmlunicodeN (fn (name, _) => span name);
    84 
    85 end;