diff options
| author | Hugo Herbelin | 2018-06-10 10:53:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-06-29 19:14:07 +0200 |
| commit | e3a7caa0fb44f7a12248a140528462853810a614 (patch) | |
| tree | 6b8efab5834d07308ecd5b2cc19a810d13c376a1 | |
| parent | d46dd57462650d1e956d8e80d5aa4e537205de4d (diff) | |
Workaround to fix #7731 (printing not splitting line at break hint).
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
| -rw-r--r-- | test-suite/output/Notations3.out | 5 | ||||
| -rw-r--r-- | test-suite/output/Notations3.v | 14 | ||||
| -rw-r--r-- | vernac/metasyntax.ml | 11 |
3 files changed, 28 insertions, 2 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 996af59270..5ab616160a 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -241,3 +241,8 @@ Notation Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3cf0c913f7..876aaa3944 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -385,3 +385,17 @@ Module LocateNotations. Locate "exists". Locate "( _ , _ , .. , _ )". End LocateNotations. + +Module Issue7731. + +Axiom (P : nat -> Prop). +Parameter (X : nat). +Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'"). +Notation "%" := X. + +Set Printing Width 7. +Goal ## @ % ^^^. +Show. +Abort. + +End Issue7731. diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index da14358ef5..c361eb4dc6 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 |