From 87a8d6c24fa5d014380340fc09647bcd53b9fb5e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 22 Aug 2017 01:19:13 +0200 Subject: Being more flexible on format Adding a warning to be more informative --- vernac/metasyntax.ml | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'vernac') 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 -- cgit v1.2.3