Mise en place de motifs récursifs dans Notation; quelques simplifications au passage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5510 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 25 insertions, 6 deletions

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 753ac89ddf..164889adf8 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -61,17 +61,32 @@ let env_assoc_value v env =
   try List.nth env (v-1)
   with Not_found -> anomaly ("Inconsistent environment for pretty-print rule")
 
+let decode_constrlist_value = function
+  | CAppExpl (_,_,l) -> l
+  | CApp (_,_,l) -> List.map fst l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
+let decode_patlist_value = function
+  | CPatCstr (_,_,l) -> l
+  | _ -> anomaly "Ill-formed list argument of notation"
+
 open Symbols
 
-let rec print_hunk n pr env = function
+let rec print_hunk n decode pr env = function
   | UnpMetaVar (e,prec) -> pr (n,prec) (env_assoc_value e env)
+  | UnpListMetaVar (e,prec,sl) -> 
+      prlist_with_sep (fun () -> prlist (print_hunk n decode pr env) sl)
+      (pr (n,prec)) (decode (env_assoc_value e env))
   | UnpTerminal s -> str s
-  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n pr env) sub)
+  | UnpBox (b,sub) -> ppcmd_of_box b (prlist (print_hunk n decode pr env) sub)
   | UnpCut cut -> ppcmd_of_cut cut
 
-let pr_notation pr s env =
+let pr_notation_gen decode pr s env =
   let unpl, level = find_notation_printing_rule s in
-  prlist (print_hunk level pr env) unpl, level
+  prlist (print_hunk level decode pr env) unpl, level
+
+let pr_notation = pr_notation_gen decode_constrlist_value
+let pr_patnotation = pr_notation_gen decode_patlist_value
 
 let pr_delimiters key strm =
   strm ++ str ("%"^key)
@@ -154,7 +169,7 @@ let rec pr_patt sep inh p =
   | CPatAtom (_,Some r) -> pr_reference r, latom
   | CPatNotation (_,"( _ )",[p]) ->
       pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom
-  | CPatNotation (_,s,env) -> pr_notation (pr_patt mt) s env
+  | CPatNotation (_,s,env) -> pr_patnotation (pr_patt mt) s env
   | CPatNumeral (_,i) -> Bignat.pr_bigint i, latom
   | CPatDelimiters (_,k,p) -> pr_delimiters k (pr_patt mt lsimple p), 1
   in
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 2fd54a006a..adfddea7b4 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -130,6 +130,7 @@ let pr_set_entry_type = function
   | ETConstr _ -> str"constr"
   | ETOther (_,e) -> str e
   | ETBigint -> str "bigint"
+  | ETConstrList _ -> failwith "Internal entry type"
 
 let pr_non_terminal = function
   | NtQual (u,nt) -> (* no more qualified entries *) str nt
@@ -522,9 +523,12 @@ let rec pr_vernac = function
 *)      
   | VernacSyntax (u,el) ->
       msgerrnl (str"Warning : Syntax is discontinued; use Notation");
-      str"(* Syntax is discontinued " ++
+      str"(* <Warning> : Syntax is discontinued" ++ 
+(*
+      fnl () ++
       hov 1 (str"Syntax " ++ str u ++ spc() ++
       prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
+*)
       str " *)"
   | VernacOpenCloseScope (local,opening,sc) ->
       str (if opening then "Open " else "Close ") ++ pr_locality local ++