From 5b4e169dada3cc5c9fd88b797291cfffb9518da2 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 16 Jan 2003 21:13:16 +0000
Subject: Bugs affichage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3517 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/metasyntax.ml | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6c99d24516..5a4c2fd65e 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
-- 
cgit v1.2.3