tuned dest_lexicon;
authorwenzelm
Fri Jul 16 22:25:07 1999 +0200 (1999-07-16)
changeset 7025afbd8241797b
parent 7024 44bd3c094fd6
child 7026 69724548fad1
tuned dest_lexicon;
src/Pure/General/scan.ML
src/Pure/Syntax/syntax.ML
     1.1 --- a/src/Pure/General/scan.ML	Fri Jul 16 22:24:42 1999 +0200
     1.2 +++ b/src/Pure/General/scan.ML	Fri Jul 16 22:25:07 1999 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4    val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     1.5    val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a
     1.6    type lexicon
     1.7 -  val dest_lexicon: lexicon -> string list list
     1.8 +  val dest_lexicon: lexicon -> string list
     1.9    val make_lexicon: string list list -> lexicon
    1.10    val empty_lexicon: lexicon
    1.11    val extend_lexicon: lexicon -> string list list -> lexicon
    1.12 @@ -240,11 +240,13 @@
    1.13  
    1.14  (* dest_lexicon *)
    1.15  
    1.16 -fun dest_lexicon Empty = []
    1.17 -  | dest_lexicon (Branch (_, [], lt, eq, gt)) =
    1.18 -      dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt
    1.19 -  | dest_lexicon (Branch (_, cs, lt, eq, gt)) =
    1.20 -      dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt;
    1.21 +fun dest_lex Empty = []
    1.22 +  | dest_lex (Branch (_, [], lt, eq, gt)) =
    1.23 +      dest_lex lt @ dest_lex eq @ dest_lex gt
    1.24 +  | dest_lex (Branch (_, cs, lt, eq, gt)) =
    1.25 +      dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt;
    1.26 +
    1.27 +val dest_lexicon = map implode o dest_lex;
    1.28  
    1.29  
    1.30  (* empty, extend, make, merge lexicons *)
    1.31 @@ -265,14 +267,14 @@
    1.32  	      Branch (c, no_literal, Empty, add Empty cs, Empty)
    1.33  	  | add lex [] = lex;
    1.34        in add lex chrs end;
    1.35 -  in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end;
    1.36 +  in foldl ext (lexicon, chrss \\ dest_lex lexicon) end;
    1.37  
    1.38  val make_lexicon = extend_lexicon empty_lexicon;
    1.39  
    1.40  fun merge_lexicons lex1 lex2 =
    1.41    let
    1.42 -    val chss1 = dest_lexicon lex1;
    1.43 -    val chss2 = dest_lexicon lex2;
    1.44 +    val chss1 = dest_lex lex1;
    1.45 +    val chss2 = dest_lex lex2;
    1.46    in
    1.47      if chss2 subset chss1 then lex1
    1.48      else if chss1 subset chss2 then lex2
     2.1 --- a/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:24:42 1999 +0200
     2.2 +++ b/src/Pure/Syntax/syntax.ML	Fri Jul 16 22:25:07 1999 +0200
     2.3 @@ -281,7 +281,7 @@
     2.4      val {lexicon, logtypes, prmodes, gram, prtabs, ...} = tabs;
     2.5      val prmodes' = sort_strings (filter_out (equal "") prmodes);
     2.6    in
     2.7 -    Pretty.writeln (pretty_strs_qs "lexicon:" (map implode (Scan.dest_lexicon lexicon)));
     2.8 +    Pretty.writeln (pretty_strs_qs "lexicon:" (Scan.dest_lexicon lexicon));
     2.9      Pretty.writeln (Pretty.strs ("logtypes:" :: logtypes));
    2.10      Pretty.writeln (Pretty.big_list "prods:" (Parser.pretty_gram gram));
    2.11      Pretty.writeln (pretty_strs_qs "print modes:" prmodes')