From f917f05b16a6c6e6d7282ffa9c788808935fd837 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Dec 2003 22:15:36 +0000
Subject: 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
---
 toplevel/metasyntax.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a18659cc25..713127c767 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
-- 
cgit v1.2.3