src/Pure/Syntax/parser.ML
changeset 77723 b761c91c2447
parent 71468 53fcbede7bf7
child 77741 1951f6470792
equal deleted inserted replaced
77722:8faf28a80a7f 77723:b761c91c2447
    36 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
    36 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
    37 fun tags_lookup (tags: tags) = Symtab.lookup tags;
    37 fun tags_lookup (tags: tags) = Symtab.lookup tags;
    38 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
    38 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
    39 fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
    39 fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));
    40 
    40 
    41 type nts = Inttab.set;
    41 type nts = Intset.T;
    42 val nts_empty: nts = Inttab.empty;
    42 val nts_empty: nts = Intset.empty;
    43 val nts_merge: nts * nts -> nts = Inttab.merge (K true);
    43 val nts_merge: nts * nts -> nts = Intset.merge;
    44 fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
    44 fun nts_insert nt : nts -> nts = Intset.insert nt;
    45 fun nts_member (nts: nts) = Inttab.defined nts;
    45 fun nts_member (nts: nts) = Intset.member nts;
    46 fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
    46 fun nts_fold f (nts: nts) = Intset.fold f nts;
    47 fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
    47 fun nts_subset (nts1: nts, nts2: nts) = Intset.forall (nts_member nts2) nts1;
    48 fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
    48 fun nts_is_empty (nts: nts) = Intset.is_empty nts;
    49 fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
    49 fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Intset.is_single nts;
    50 
    50 
    51 
    51 
    52 (* tokens *)
    52 (* tokens *)
    53 
    53 
    54 structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
    54 structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);