src/Tools/WWW_Find/unicode_symbols.ML
changeset 50135 d5132bba6a83
parent 48992 0518bf89c777
child 50136 a96bd08258a2
equal deleted inserted replaced
50134:13211e07d931 50135:d5132bba6a83
     1 (*  Title:      Tools/WWW_Find/unicode_symbols.ML
     1 (*  Title:      Tools/WWW_Find/unicode_symbols.ML
     2     Author:     Timothy Bourke, NICTA
     2     Author:     Timothy Bourke, NICTA
     3 
     3 
     4 Parse the ISABELLE_HOME/etc/symbols file.
     4 Ad-hoc parsing of ~~/etc/symbols.
     5 *)
     5 *)
     6 
     6 
     7 signature UNICODE_SYMBOLS =
     7 signature UNICODE_SYMBOLS =
     8 sig
     8 sig
     9 val symbol_to_unicode : string -> int option
     9   val symbol_to_unicode : string -> int option
    10 val abbrev_to_unicode : string -> int option
    10   val abbrev_to_unicode : string -> int option
    11 val unicode_to_symbol : int -> string option
    11   val unicode_to_symbol : int -> string option
    12 val unicode_to_abbrev : int -> string option
    12   val unicode_to_abbrev : int -> string option
    13 val utf8_to_symbols   : string -> string
    13   val utf8_to_symbols : string -> string
    14 val utf8              : int list -> string
    14   val utf8 : int list -> string
    15 end;
    15 end;
    16 
    16 
    17 structure UnicodeSymbols : UNICODE_SYMBOLS =
    17 structure UnicodeSymbols : UNICODE_SYMBOLS =
    18 struct
    18 struct
    19 
    19 
   132 val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
   132 val abbr = Scan.option ($$$ "abbrev" -- $$$ ":"
   133                         |-- (ascii_sym || $$$ ":" || name));
   133                         |-- (ascii_sym || $$$ ":" || name));
   134 
   134 
   135 in
   135 in
   136 
   136 
   137 val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
   137 val line = (symbol -- unicode -- font -- abbr) >> (fn (((a, b), c), d) => (a, b, d));
   138 
   138 
   139 end;
   139 end;
   140 
   140 
   141 local (* build tables *)
   141 local (* build tables *)
   142 
   142