equal
deleted
inserted
replaced
94 |
94 |
95 |
95 |
96 (** tables of token translation functions **) |
96 (** tables of token translation functions **) |
97 |
97 |
98 fun lookup_tokentr tabs modes = |
98 fun lookup_tokentr tabs modes = |
99 let val trs = distinct_fst_string (flat (map (assocs tabs) (modes @ [""]))) |
99 let val trs = gen_distinct eq_fst (flat (map (assocs tabs) (modes @ [""]))) |
100 in fn c => apsome fst (assoc (trs, c)) end; |
100 in fn c => apsome fst (assoc (trs, c)) end; |
101 |
101 |
102 fun merge_tokentrtabs tabs1 tabs2 = |
102 fun merge_tokentrtabs tabs1 tabs2 = |
103 let |
103 let |
104 fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2; |
104 fun eq_tr ((c1, (_, s1)), (c2, (_, s2))) = c1 = c2 andalso s1 = s2; |