diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-16 21:13:16 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-16 21:13:16 +0000 |
| commit | 5b4e169dada3cc5c9fd88b797291cfffb9518da2 (patch) | |
| tree | 02cf1870d8574a59f0e34b931ca2d54d7852f452 /toplevel | |
| parent | 0c52732d2b89604b9ba0f1b1b2643111bde47c0d (diff) | |
Bugs affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 6c99d2451..5a4c2fd65 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -288,7 +288,11 @@ let make_hunks_ast symbols etyps from = add_break (if protect then 1 else 0) (RO (if protect then s^" " else s) :: make CanBreak prods) else - RO s :: make CanBreak prods + if protect then + (if ws = CanBreak then add_break 1 else (fun x -> x)) + (RO (s^" ") :: make CanBreak prods) + else + RO s :: make CanBreak prods | Terminal s :: prods -> RO s :: make NoBreak prods @@ -326,7 +330,11 @@ let make_hunks etyps symbols = add_break (if protect then 1 else 0) (UnpTerminal (if protect then s^" " else s) :: make CanBreak prods) else - UnpTerminal s :: make CanBreak prods + if protect then + (if ws = CanBreak then add_break 1 else (fun x -> x)) + (UnpTerminal (s^" ") :: make CanBreak prods) + else + UnpTerminal s :: make CanBreak prods | Terminal s :: prods -> UnpTerminal s :: make NoBreak prods |