From 12f4cb9c189bd70a6cd252a5269b6d3c7d327667 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Sat, 5 Aug 2017 22:13:21 +0200
Subject: 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.
---
 test-suite/bugs/closed/5469.v |  3 ---
 vernac/metasyntax.ml          | 31 ++-----------------------------
 2 files changed, 2 insertions(+), 32 deletions(-)
 delete mode 100644 test-suite/bugs/closed/5469.v

diff --git a/test-suite/bugs/closed/5469.v b/test-suite/bugs/closed/5469.v
deleted file mode 100644
index fce671c75..000000000
--- a/test-suite/bugs/closed/5469.v
+++ /dev/null
@@ -1,3 +0,0 @@
-(* Some problems with the special treatment of curly braces *)
-
-Reserved Notation "'a' { x }" (at level 0, format "'a' { x }").
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''
-- 
cgit v1.2.3