diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-01 02:11:49 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-01 02:11:49 +0200 |
| commit | 09bc93c7faf59de7d8219d6c675300c522129404 (patch) | |
| tree | 3c3ca760d41c47139507cb6f4c5d3973c51dd0ac /vernac | |
| parent | 74640d2b8bc158b301c0646db19747a86313e25a (diff) | |
| parent | e3a7caa0fb44f7a12248a140528462853810a614 (diff) | |
Merge PR #7759: Workaround to fix #7731 (printing not splitting line at break hint).
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef..c361eb4dc 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1312,8 +1312,15 @@ let make_pa_rule level (typs,symbols) ntn need_squash = let make_pp_rule level (typs,symbols) fmt = match fmt with - | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)] - | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt) + | None -> + let hunks = make_hunks typs symbols level in + if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then + [UnpBox (PpHOVB 0,hunks)] + else + (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *) + List.map snd hunks (* drop locations which are dummy *) + | Some fmt -> + hunks_of_format (level, List.split typs) (symbols, parse_format fmt) (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *) let make_syntax_rules (sd : SynData.syn_data) = let open SynData in |