Prise en compte des notations récursives dans l'option 'format'

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

2 files changed, 41 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 4862cd1197..f0f9c437e9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,10 @@ Ltac
 - New modifier "lazy" for "match t with" and "match goal with" telling
   to delay the evaluation of tactic expression.
 
+Notations
+
+- "format" option aware of recursive notations
+
 Changes from V8.0beta to V8.0
 =============================
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 563fa309c8..bc037f851b 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -606,6 +606,41 @@ let make_hunks etyps symbols from =
 
   in make NoBreak symbols
 
+let error_format () = error "The format does not match the notation"
+
+let rec split_format_at_ldots hd = function
+  | UnpTerminal s :: fmt when id_of_string s = ldots_var -> List.rev hd, fmt
+  | u :: fmt -> 
+      check_no_ldots_in_box u;
+      split_format_at_ldots (u::hd) fmt
+  | [] -> raise Exit
+
+and check_no_ldots_in_box = function
+  | UnpBox (_,fmt) ->
+      (try 
+        let _ = split_format_at_ldots [] fmt in
+        error ("The special symbol \"..\" must occur at the same formatting depth than the variables of which it is the ellipse")
+      with Exit -> ())
+  | _ -> ()
+
+let skip_var_in_recursive_format = function
+  | UnpTerminal _ :: sl (* skip first var *) ->
+      (* To do, though not so important: check that the names match
+         the names in the notation *)
+      sl
+  | _ -> error_format ()
+
+let read_recursive_format sl fmt =
+  let get_head fmt =
+    let sl = skip_var_in_recursive_format fmt in
+    try split_format_at_ldots [] sl with Exit -> error_format () in
+  let rec get_tail = function
+    | a :: sepfmt, b :: fmt when a = b -> get_tail (sepfmt, fmt)
+    | [], tail -> skip_var_in_recursive_format tail
+    | _ -> error "The format is not the same on the right and left hand side of the special token \"..\"" in
+  let slfmt, fmt = get_head fmt in
+  slfmt, get_tail (slfmt, fmt)
+
 let hunks_of_format (from,(vars,typs) as vt) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
@@ -625,11 +660,11 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
   | symbs, (UnpCut _ as u) :: fmt ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
   | symbs, [] -> symbs, []
-  | _, _ -> error "The format does not match the notation"
+  | _, _ -> error_format ()
   in
   match aux symfmt with
   | [], l -> l
-  | _ -> error "The format does not match the notation"
+  | _ -> error_format ()
 
 let string_of_prec (n,p) =
   (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")