diff options
| author | herbelin | 2011-04-28 07:11:36 +0000 |
|---|---|---|
| committer | herbelin | 2011-04-28 07:11:36 +0000 |
| commit | 60dcc820b206ac0540af248ee993bfd000ba7bf0 (patch) | |
| tree | 42b98db64e65ace3037c00c9fbafd1b941cf7389 | |
| parent | 98549131f0fead9cdb1a785210775d057db7a417 (diff) | |
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
| -rw-r--r-- | test-suite/output/InitSyntax.out | 2 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 14 |
2 files changed, 9 insertions, 7 deletions
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index 9299e01046..c251b1b1ce 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -1,5 +1,5 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := - exist2 : forall x : A, P x -> Q x -> sig2 P Q + exist2 : forall x : A, P x -> Q x -> {x | P x & Q x } For sig2: Argument A is implicit For exist2: Argument A is implicit 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 |