diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 22:15:36 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-12-19 22:15:36 +0000 |
| commit | f917f05b16a6c6e6d7282ffa9c788808935fd837 (patch) | |
| tree | cdc037847e756f5db5892c196f5ecc43f8b339ca /toplevel/metasyntax.ml | |
| parent | 3f1770caeed7daa296db9062fbce28f869bb8379 (diff) | |
Suppression de l'espace avant les notations commencant par un ident
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5118 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index a18659cc2..713127c76 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -512,11 +512,15 @@ let make_hunks etyps symbols from = UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods) else UnpTerminal s :: add_break 1 (make NoBreak prods) - else - if ws = CanBreak or is_ident_tail s.[String.length s - 1] then + else if is_ident_tail s.[String.length s - 1] then + if ws = CanBreak then add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) else - UnpTerminal s :: make CanBreak prods + UnpTerminal (s^" ") :: make CanBreak prods + else if ws = CanBreak then + add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) + else + UnpTerminal s :: make CanBreak prods | Terminal s :: prods -> if is_right_bracket s then |