equal
deleted
inserted
replaced
82 fun update_abbrevs mode abbrs = |
82 fun update_abbrevs mode abbrs = |
83 Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs); |
83 Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs); |
84 |
84 |
85 fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = |
85 fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes = |
86 let val nets = map_filter (Symtab.lookup rev_abbrevs) modes |
86 let val nets = map_filter (Symtab.lookup rev_abbrevs) modes |
87 in fn t => maps (fn net => Item_Net.retrieve net t) nets end; |
87 in fn t => maps (fn net => Item_Net.retrieve_matching net t) nets end; |
88 |
88 |
89 |
89 |
90 (* dest consts *) |
90 (* dest consts *) |
91 |
91 |
92 fun dest (Consts {decls, constraints, ...}) = |
92 fun dest (Consts {decls, constraints, ...}) = |