src/Tools/WWW_Find/unicode_symbols.ML
changeset 43602 8c89a1fb30f2
parent 43485 33a24212a72d
child 43947 9b00f09f7721
equal deleted inserted replaced
43601:fd650d659275 43602:8c89a1fb30f2
   133 
   133 
   134 in
   134 in
   135 
   135 
   136 val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
   136 val line = (symbol -- unicode --| font -- abbr) >> Parse.triple1;
   137 
   137 
   138 val symbols_path =
       
   139   [getenv "ISABELLE_HOME", "etc", "symbols"]
       
   140   |> map Path.explode
       
   141   |> Path.appends;
       
   142 
       
   143 end;
   138 end;
   144 
   139 
   145 local (* build tables *)
   140 local (* build tables *)
   146 
   141 
   147 fun add_entries ((fromsym, fromabbr, tosym, toabbr), ((sym, pos), uni, oabbr)) =
   142 fun add_entries ((fromsym, fromabbr, tosym, toabbr), ((sym, pos), uni, oabbr)) =
   162 in
   157 in
   163 
   158 
   164 fun read_symbols path =
   159 fun read_symbols path =
   165   let
   160   let
   166     val parsed_lines =
   161     val parsed_lines =
   167       File.read path
   162       Symbol_Pos.explode (File.read path, Path.position path)
   168       |> (fn x => Symbol_Pos.explode (x, Position.file (Path.implode path)))
       
   169       |> tokenize
   163       |> tokenize
   170       |> filter is_proper
   164       |> filter is_proper
   171       |> Scan.finite stopper (Scan.repeat line)
   165       |> Scan.finite stopper (Scan.repeat line)
   172       |> fst;
   166       |> fst;
   173   in
   167   in
   177   end;
   171   end;
   178 
   172 
   179 end;
   173 end;
   180 
   174 
   181 local
   175 local
   182 val (fromsym, fromabbr, tosym, toabbr) = read_symbols symbols_path;
   176 val (fromsym, fromabbr, tosym, toabbr) = read_symbols (Path.explode "~~/etc/symbols");
   183 in
   177 in
   184 val symbol_to_unicode = Symtab.lookup fromsym;
   178 val symbol_to_unicode = Symtab.lookup fromsym;
   185 val abbrev_to_unicode = Symtab.lookup fromabbr;
   179 val abbrev_to_unicode = Symtab.lookup fromabbr;
   186 val unicode_to_symbol = Inttab.lookup tosym;
   180 val unicode_to_symbol = Inttab.lookup tosym;
   187 val unicode_to_abbrev = Inttab.lookup toabbr;
   181 val unicode_to_abbrev = Inttab.lookup toabbr;