diff options
| author | Jim Fehrle | 2020-10-16 21:12:49 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-10-19 11:49:31 -0700 |
| commit | 48e0d4112cdf23ec89e8044387bd8484cb026b92 (patch) | |
| tree | b50fda16e2e1343f632937d213b99ba9f54e9742 | |
| parent | 07a199ffa640b9eb94235ebc3732c4b2981ca525 (diff) | |
Better message and avoid an infinite SPLICE loop
| -rw-r--r-- | doc/tools/docgram/doc_grammar.ml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index 0ac652c0db..177abe53fc 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -909,14 +909,17 @@ let apply_splice g edit_map = List.iter (fun b -> let (nt0, prods0) = b in let rec splice_loop nt prods cnt = - let max_cnt = 10 in - let (nt', prods') = edit_rule g edit_map nt prods in - if cnt > max_cnt then - error "Splice for '%s' not done after %d iterations\n" nt0 max_cnt; - if nt' = nt && prods' = prods then - (nt', prods') - else - splice_loop nt' prods' (cnt+1) + if cnt >= 10 then begin + error "Splice for '%s' not done after %d iterations. Current value is:\n" nt0 cnt; + List.iter (fun prod -> Printf.eprintf " %s\n" (prod_to_str prod)) prods; + (nt, prods) + end else begin + let (nt', prods') = edit_rule g edit_map nt prods in + if nt' = nt && prods' = prods then + (nt, prods) + else + splice_loop nt' prods' (cnt+1) + end in let (nt', prods') = splice_loop nt0 prods0 0 in g_update_prods g nt' prods') |