src/Tools/WWW_Find/unicode_symbols.ML
changeset 48992 0518bf89c777
parent 43947 9b00f09f7721
child 50135 d5132bba6a83
equal deleted inserted replaced
48991:0350245dec1c 48992:0518bf89c777
   107   in
   107   in
   108     (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
   108     (case Scan.error (Scan.finite Symbol_Pos.stopper scan_token) syms of
   109       (toks, []) => toks
   109       (toks, []) => toks
   110     | (_, ss) =>
   110     | (_, ss) =>
   111         error ("Lexical error at: " ^ Symbol_Pos.content ss ^
   111         error ("Lexical error at: " ^ Symbol_Pos.content ss ^
   112           Position.str_of (#1 (Symbol_Pos.range ss))))
   112           Position.here (#1 (Symbol_Pos.range ss))))
   113   end;
   113   end;
   114 
   114 
   115 val stopper =
   115 val stopper =
   116   Scan.stopper
   116   Scan.stopper
   117     (fn [] => mk_eof Position.none
   117     (fn [] => mk_eof Position.none
   150    | SOME abbr =>
   150    | SOME abbr =>
   151        (Symtab.update_new (sym, uni) fromsym,
   151        (Symtab.update_new (sym, uni) fromsym,
   152         Symtab.update_new (abbr, uni) fromabbr,
   152         Symtab.update_new (abbr, uni) fromabbr,
   153         Inttab.update (uni, sym) tosym,
   153         Inttab.update (uni, sym) tosym,
   154         Inttab.update (uni, abbr) toabbr))
   154         Inttab.update (uni, abbr) toabbr))
   155   handle Symtab.DUP sym => error ("Duplicate at" ^ Position.str_of pos)
   155   handle Symtab.DUP sym => error ("Duplicate at" ^ Position.here pos)
   156        | Inttab.DUP sym => error ("Duplicate code at" ^ Position.str_of pos);
   156        | Inttab.DUP sym => error ("Duplicate code at" ^ Position.here pos);
   157 
   157 
   158 in
   158 in
   159 
   159 
   160 fun read_symbols path =
   160 fun read_symbols path =
   161   let
   161   let