aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
Diffstat (limited to 'vernac')
-rw-r--r--vernac/metasyntax.ml7
1 files changed, 7 insertions, 0 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e142f2ab8..1b9cfc07e 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -504,6 +504,12 @@ let make_hunks etyps symbols from =
let error_format ?loc () = user_err ?loc Pp.(str "The format does not match the notation.")
+let warn_format_break =
+ CWarnings.create ~name:"notation-both-format-and-spaces" ~category:"parsing"
+ (fun () ->
+ strbrk "Discarding format implicitly indicated by multiple spaces in notation because an explicit format modifier is given.")
+
+
let rec split_format_at_ldots hd = function
| (loc,UnpTerminal s) :: fmt when String.equal s (Id.to_string ldots_var) -> loc, List.rev hd, fmt
| u :: fmt ->
@@ -575,6 +581,7 @@ let hunks_of_format (from,(vars,typs)) symfmt =
| _ -> assert false in
symbs, hunk :: l
| symbs, [] -> symbs, []
+ | Break _ :: symbs, fmt -> warn_format_break (); aux (symbs,fmt)
| _, fmt -> error_format ?loc:(fst (List.hd fmt)) ()
in
match aux symfmt with