diff options
| author | herbelin | 2003-04-10 21:50:43 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-10 21:50:43 +0000 |
| commit | 463531101b7db0a47c49242346f6e765b3cec3b4 (patch) | |
| tree | 0161f90fc2409daf7c139710ad1a3a72084ac82d | |
| parent | 74503ecc689d8da84491330307fd2ba82683c9c3 (diff) | |
Suppression de quelques espaces superflus
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3908 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 32 |
1 files changed, 22 insertions, 10 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 726f521c17..fa0310c003 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -256,7 +256,7 @@ let is_operator s = let l = String.length s in l <> 0 & (s.[0] = '+' or s.[0] = '*' or s.[0] = '=' or s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or - s.[0] = '@') + s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~') type previous_prod_status = NoBreak | CanBreak @@ -320,19 +320,31 @@ let make_hunks etyps symbols = u :: make CanBreak prods | Terminal s :: prods when List.exists is_non_terminal prods -> - if ws = CanBreak then - if is_comma s || is_right_bracket s then - UnpTerminal s :: add_break 1 (make NoBreak prods) - else if is_operator s then - UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods) + if is_comma s then + UnpTerminal s :: add_break 1 (make NoBreak prods) + else if is_right_bracket s then + UnpTerminal s :: add_break 0 (make NoBreak prods) + else if is_left_bracket s then + if ws = CanBreak then + add_break 1 (UnpTerminal s :: make CanBreak prods) else + UnpTerminal s :: make CanBreak prods + else if is_operator s then + if ws = CanBreak then + UnpTerminal (" "^s) :: add_break 1 (make NoBreak prods) + else + UnpTerminal s :: add_break 1 (make NoBreak prods) + else + if ws = CanBreak then add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods) - else - UnpTerminal (s^" ") :: make CanBreak prods + else + UnpTerminal (s^" ") :: make CanBreak prods | Terminal s :: prods -> - if ws = CanBreak then - UnpTerminal (" "^s) :: make NoBreak prods + if is_right_bracket s then + UnpTerminal s ::make NoBreak prods + else if ws = CanBreak then + add_break 1 (UnpTerminal s :: make NoBreak prods) else UnpTerminal s :: make NoBreak prods |