From 060efb7940d6bea8cb72659e6d16c65443f2e1e7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 9 Oct 2006 17:47:59 +0000
Subject: Amélioration de l'automatisation des coupures quand deux idents se
 suivent

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

diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a22f99c39c..18ff746f1c 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -399,6 +399,10 @@ let is_operator s =
    s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
    s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~')
 
+let is_prod_ident = function
+  | Terminal s when is_letter s.[0] or s.[0] = '_' -> true
+  | _ -> false
+
 let rec is_non_terminal = function
   | NonTerminal _ | SProdList _ -> true
   | _ -> false
@@ -437,10 +441,11 @@ let make_hunks etyps symbols from =
 	  else 
 	    UnpTerminal s :: add_break 1 (make NoBreak prods)
 	else if is_ident_tail s.[String.length s - 1] then
+	  let sep = if is_prod_ident (List.hd prods) then "" else " " in
 	  if ws = CanBreak then
-	    add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
+	    add_break 1 (UnpTerminal (s^sep) :: make CanBreak prods)
 	  else
-	    UnpTerminal (s^" ") :: make CanBreak prods
+	    UnpTerminal (s^sep) :: make CanBreak prods
 	else if ws = CanBreak then
 	  add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
 	else
-- 
cgit v1.2.3