# HG changeset patch # User wenzelm # Date 932156707 -7200 # Node ID afbd8241797b6515baf643e931245c6c4c5ead39 # Parent 44bd3c094fd6e98be604e5b6cbeb62ec3d640d5f tuned dest_lexicon; diff -r 44bd3c094fd6 -r afbd8241797b src/Pure/General/scan.ML --- a/src/Pure/General/scan.ML Fri Jul 16 22:24:42 1999 +0200 +++ b/src/Pure/General/scan.ML Fri Jul 16 22:25:07 1999 +0200 @@ -60,7 +60,7 @@ val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a type lexicon - val dest_lexicon: lexicon -> string list list + val dest_lexicon: lexicon -> string list val make_lexicon: string list list -> lexicon val empty_lexicon: lexicon val extend_lexicon: lexicon -> string list list -> lexicon @@ -240,11 +240,13 @@ (* dest_lexicon *) -fun dest_lexicon Empty = [] - | dest_lexicon (Branch (_, [], lt, eq, gt)) = - dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt - | dest_lexicon (Branch (_, cs, lt, eq, gt)) = - dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt; +fun dest_lex Empty = [] + | dest_lex (Branch (_, [], lt, eq, gt)) = + dest_lex lt @ dest_lex eq @ dest_lex gt + | dest_lex (Branch (_, cs, lt, eq, gt)) = + dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt; + +val dest_lexicon = map implode o dest_lex; (* empty, extend, make, merge lexicons *) @@ -265,14 +267,14 @@ Branch (c, no_literal, Empty, add Empty cs, Empty) | add lex [] = lex; in add lex chrs end; - in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; + in foldl ext (lexicon, chrss \\ dest_lex lexicon) end; val make_lexicon = extend_lexicon empty_lexicon; fun merge_lexicons lex1 lex2 = let - val chss1 = dest_lexicon lex1; - val chss2 = dest_lexicon lex2; + val chss1 = dest_lex lex1; + val chss2 = dest_lex lex2; in if chss2 subset chss1 then lex1 else if chss1 subset chss2 then lex2 diff -r 44bd3c094fd6 -r afbd8241797b src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Fri Jul 16 22:24:42 1999 +0200 +++ b/src/Pure/Syntax/syntax.ML Fri Jul 16 22:25:07 1999 +0200 @@ -281,7 +281,7 @@ val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs; val prmodes' = sort_strings (filter_out (equal "") prmodes); in - Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon))); + Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon)); Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes)); Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram)); Pretty.writeln (pretty_strs_qs "print modes:" prmodes')