aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-10 10:53:32 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-06-29 19:14:07 +0200
commite3a7caa0fb44f7a12248a140528462853810a614 (patch)
tree6b8efab5834d07308ecd5b2cc19a810d13c376a1
parentd46dd57462650d1e956d8e80d5aa4e537205de4d (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.out5
-rw-r--r--test-suite/output/Notations3.v14
-rw-r--r--vernac/metasyntax.ml11
3 files changed, 28 insertions, 2 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 996af5927..5ab616160 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 3cf0c913f..876aaa394 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 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