Fixed notation printing bug when curly brackets are involved (requests

for adding spaces were not taken into account in notations containing
patterns of the form "{ ident symbol", paradoxically resulting in
adding extra spaces, e.g. when printing the type "{ x |  P x }" of
"exist", due to interferences with the heuristic for adding breaking
points in Metasyntax.make_hunk).

Also adapted output of test InitSyntax.v after commit r14018 improved
the printing of "ex P" and "sig P".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 6 deletions

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index e3aaaa5e98..79b3dac5f7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -878,15 +878,17 @@ specially and require that the notation \"{ _ }\" is already reserved."
 
 (* Remove patterns of the form "{ _ }", unless it is the "{ _ }" notation *)
 let remove_curly_brackets l =
-  let rec next = function
-    | Break _ :: l -> next l
-    | l -> l in
+  let rec skip_break acc = function
+    | Break _ as br :: l -> skip_break (br::acc) l
+    | l -> List.rev acc, l in
   let rec aux deb = function
   | [] -> []
   | Terminal "{" as t1 :: l ->
-      (match next l with
+      let br,next = skip_break [] l in
+      (match next with
         | NonTerminal _ as x :: l' as l0 ->
-            (match next l' with
+            let br',next' = skip_break [] l' in
+            (match next' with
               | Terminal "}" as t2 :: l'' as l1 ->
                   if l <> l0 or l' <> l1 then
                     warning "Skipping spaces inside curly brackets";
@@ -894,7 +896,7 @@ let remove_curly_brackets l =
                     check_curly_brackets_notation_exists ();
                     x :: aux false l''
                   end
-              | l1 -> t1 :: x :: aux false l1)
+              | l1 -> t1 :: br @ x :: br' @ aux false l1)
         | l0 -> t1 :: aux false l0)
   | x :: l -> x :: aux false l
   in aux true l