# HG changeset patch
# User clasohm
# Date 769949752 -7200
# Node ID 712dceb1ecc790346f99af846dcbd1a2cc3f7b73
# Parent  432bb99958939c5b4462f41e560b858cadf9c416
"Building new grammar" message is no longer displayed by empty_gram

diff -r 432bb9995893 -r 712dceb1ecc7 src/Pure/Syntax/parser.ML
--- a/src/Pure/Syntax/parser.ML	Tue May 24 09:04:03 1994 +0200
+++ b/src/Pure/Syntax/parser.ML	Thu May 26 12:55:52 1994 +0200
@@ -51,9 +51,7 @@
 (* convert productions to reference grammar with lookaheads and eliminate
    chain productions *)
 fun mk_gram prods =
-  let val _ = writeln "Building new grammar...";
-
-      (*get reference on list of all possible rhss for nonterminal lhs
+  let (*get reference on list of all possible rhss for nonterminal lhs
         (if it doesn't exist a new one is created and added to the nonterminal
          list)*)
       fun get_rhss ref_prods lhs =
@@ -277,13 +275,15 @@
     val prods2 = distinct (map prod_of xprods2);
   in
     if prods2 subset prods1 then gram1
-    else mk_gram (extend_list prods1 prods2)
+    else (writeln "Building new grammar...";
+          mk_gram (extend_list prods1 prods2))
   end;
 
 fun merge_grams (gram1 as Gram (prods1, _)) (gram2 as Gram (prods2, _)) =
   if prods2 subset prods1 then gram1
   else if prods1 subset prods2 then gram2
-  else mk_gram (merge_lists prods1 prods2);
+  else (writeln "Building new grammar...";
+        mk_gram (merge_lists prods1 prods2));
 
 
 (* pretty_gram *)