diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-05 22:13:21 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-29 05:18:49 +0200 |
commit | 12f4cb9c189bd70a6cd252a5269b6d3c7d327667 (patch) | |
tree | 0a2f312803f87ab5eaf9c7ca742f8ceda91e2f47 /vernac/metasyntax.ml | |
parent | f442efebd8354b233827e4991a80d27082c772e1 (diff) |
Dropping former fix to bug #5469 (notation format not recognizing curly braces).
This reverts commit 53a50875 and a bit more: it also makes the check
for possibly ignoring formatting spaces irrelevant, since the previous
commit makes that curly brackets are not any more dropped for
printing.
Diffstat (limited to 'vernac/metasyntax.ml')
-rw-r--r-- | vernac/metasyntax.ml | 31 |
1 files changed, 2 insertions, 29 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 76c5dc1be..a98cff384 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -522,35 +522,11 @@ let read_recursive_format sl fmt = let slfmt, fmt = get_head fmt in slfmt, get_tail (slfmt, fmt) -let warn_skip_spaces_curly = - CWarnings.create ~name:"skip-spaces-curly" ~category:"parsing" - (fun () ->strbrk "Skipping spaces inside curly brackets") - -let rec drop_spacing = function - | UnpCut _ :: fmt -> warn_skip_spaces_curly (); drop_spacing fmt - | UnpTerminal s' :: fmt when String.equal s' (String.make (String.length s') ' ') -> warn_skip_spaces_curly (); drop_spacing fmt - | fmt -> fmt - -let has_closing_curly_brace symbs fmt = - (* TODO: recognize and fail in case a box overlaps a pair of curly braces *) - let fmt = drop_spacing fmt in - match symbs, fmt with - | NonTerminal s :: symbs, (UnpTerminal s' as u) :: fmt when Id.equal s (Id.of_string s') -> - let fmt = drop_spacing fmt in - (match fmt with - | UnpTerminal "}" :: fmt -> Some (u :: fmt) - | _ -> None) - | _ -> None - let hunks_of_format (from,(vars,typs)) symfmt = - let a = ref None in let rec aux = function | symbs, (UnpTerminal s' as u) :: fmt when String.equal s' (String.make (String.length s') ' ') -> let symbs, l = aux (symbs,fmt) in symbs, u :: l - | symbs, (UnpTerminal "{") :: fmt when (a := has_closing_curly_brace symbs fmt; !a <> None) -> - let newfmt = Option.get !a in - aux (symbs,newfmt) | Terminal s :: symbs, (UnpTerminal s') :: fmt when String.equal s (String.drop_simple_quotes s') -> let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l @@ -1054,13 +1030,10 @@ let remove_curly_brackets l = | Terminal "{" as t1 :: l -> let br,next = skip_break [] l in (match next with - | NonTerminal _ as x :: l' as l0 -> + | NonTerminal _ as x :: l' -> let br',next' = skip_break [] l' in (match next' with - | Terminal "}" as t2 :: l'' as l1 -> - if not (List.equal Notation.symbol_eq l l0) || - not (List.equal Notation.symbol_eq l' l1) then - warn_skip_spaces_curly (); + | Terminal "}" as t2 :: l'' -> if deb && List.is_empty l'' then [t1;x;t2] else begin check_curly_brackets_notation_exists (); x :: aux false l'' |