src/Pure/Syntax/parser.ML
changeset 395 712dceb1ecc7
parent 377 ab8917806779
child 552 fc92fac8b0de
     1.1 --- a/src/Pure/Syntax/parser.ML	Tue May 24 09:04:03 1994 +0200
     1.2 +++ b/src/Pure/Syntax/parser.ML	Thu May 26 12:55:52 1994 +0200
     1.3 @@ -51,9 +51,7 @@
     1.4  (* convert productions to reference grammar with lookaheads and eliminate
     1.5     chain productions *)
     1.6  fun mk_gram prods =
     1.7 -  let val _ = writeln "Building new grammar...";
     1.8 -
     1.9 -      (*get reference on list of all possible rhss for nonterminal lhs
    1.10 +  let (*get reference on list of all possible rhss for nonterminal lhs
    1.11          (if it doesn't exist a new one is created and added to the nonterminal
    1.12           list)*)
    1.13        fun get_rhss ref_prods lhs =
    1.14 @@ -277,13 +275,15 @@
    1.15      val prods2 = distinct (map prod_of xprods2);
    1.16    in
    1.17      if prods2 subset prods1 then gram1
    1.18 -    else mk_gram (extend_list prods1 prods2)
    1.19 +    else (writeln "Building new grammar...";
    1.20 +          mk_gram (extend_list prods1 prods2))
    1.21    end;
    1.22  
    1.23  fun merge_grams (gram1 as Gram (prods1, _)) (gram2 as Gram (prods2, _)) =
    1.24    if prods2 subset prods1 then gram1
    1.25    else if prods1 subset prods2 then gram2
    1.26 -  else mk_gram (merge_lists prods1 prods2);
    1.27 +  else (writeln "Building new grammar...";
    1.28 +        mk_gram (merge_lists prods1 prods2));
    1.29  
    1.30  
    1.31  (* pretty_gram *)