diff options
| author | coqbot-app[bot] | 2020-10-20 14:15:40 +0000 |
|---|---|---|
| committer | GitHub | 2020-10-20 14:15:40 +0000 |
| commit | 91e7863e64a5741b6530828c1642d765ddff41ae (patch) | |
| tree | 6ee9e729905a50b4351ada1f822d3dcce5edeb6c /doc/tools | |
| parent | 554bdc2df7e5b63bbf6fcc60c33437842d2f5541 (diff) | |
| parent | 48e0d4112cdf23ec89e8044387bd8484cb026b92 (diff) | |
Merge PR #13214: Better message for doc_grammar; avoid an infinite SPLICE loop
Reviewed-by: Zimmi48
Diffstat (limited to 'doc/tools')
| -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') |