Ajout 'Close Scope'.

Mise en place de la structure pour un modificateur 'format' de Notation.


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

5 files changed, 42 insertions, 52 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index af2a227ef..0d27fc759 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -267,7 +267,10 @@ GEXTEND Gram
 	   VernacSyntaxExtension (local,None,Some(s,modl))
 
      | IDENT "Open"; local = locality; IDENT "Scope"; 
-	 sc = IDENT -> VernacOpenScope (local,sc)
+	 sc = IDENT -> VernacOpenCloseScope (local,true, sc)
+
+     | IDENT "Close"; local = locality; IDENT "Scope"; 
+	 sc = IDENT -> VernacOpenCloseScope (local,false,sc)
 
      | IDENT "Delimits"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -288,27 +291,22 @@ GEXTEND Gram
                a8=entry_prec;
                n8=OPT natural;
 	       op8=OPT STRING;
-               mv8=OPT["("; l = LIST1 syntax_modifier SEP ","; ")" -> l] ->
+               mv8=["("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> []]
+		->
 		 (match (a8,n8,mv8,op8) with
-		   | None,None,None,None -> None
-		   | _,_,Some mv8,_ ->
-		   let (a8,n8,_) = Metasyntax.interp_infix_modifiers a8 n8 mv8
-		   in Some(a8,n8,op8)
-		   | _,_,None,_ -> Some (a8,n8,op8))
+		   | None,None,[],None -> None
+		   | _,_,mv8,_ ->
+		       Some(op8,Metasyntax.merge_modifiers a8 n8 mv8))
               | -> (* Means: rules are based on V7 rules *)
-		  Some (None,None,None) ] ->
-		let v8 = Util.option_app (function
-		  | None, None, op8 ->
-		      let op8 = match op8 with None -> op | Some op -> op in
-		      let nv8 = Util.option_app adapt_level n in
-		      let mv8 = List.map map_modl modl in
-		      let (a8,n8,_) = Metasyntax.interp_infix_modifiers a nv8
-			mv8 in (a8,n8,op8)
-		  | a8,n8,op8 ->
-		      let op8 = match op8 with None -> op | Some op -> op in
-		      (a8,n8,op8)) mv8 in
-           let (ai,ni,b) = Metasyntax.interp_infix_modifiers a n modl in
-           VernacInfix (local,ai,ni,op,p,b,v8,sc)
+		  Some (None,[]) ] ->
+		let mv = Metasyntax.merge_modifiers a n modl in
+		let v8 = Util.option_app (function (op8,mv8) ->
+		  let op8 = match op8 with None -> op | Some op -> op in
+		  let mv8 = if mv8=[] then List.map map_modl mv else mv8 in
+		  let mv8 = if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then SetLevel 10 :: mv8 else mv8 in
+		  let mv8 = if List.for_all (function SetAssoc _ -> false | _ -> true) mv8 then SetAssoc Gramext.LeftA :: mv8 else mv8 in
+		  (op8,mv8)) mv8 in
+		VernacInfix (local,(op,mv),p,v8,sc)
      | IDENT "Distfix"; local = locality; a = entry_prec; n = natural; 
 	   s = STRING; p = global; sc = OPT [ ":"; sc = IDENT -> sc ] ->
              let (a,s,c) = Metasyntax.translate_distfix a s p in
@@ -331,12 +329,6 @@ GEXTEND Gram
 		(s8,mv8)
              | -> (* Means: rules are based on V7 rules *)
 		 None, Some [] ] ->
-(*
-               let s8 = match s8 with Some s -> s | _ -> s in
-               let mv8 = match mv8 with
-                   Some mv8 -> mv8
-                 | _ -> List.map map_modl modl in
-*)
 	       let smv8 = match s8,mv8 with
 		 | None, None -> None   (* = only interpretation *)
 		 | Some s8, None -> Some (s8,[]) (* = only interp, new s *)
@@ -352,9 +344,8 @@ GEXTEND Gram
      | IDENT "V8Infix"; local = locality; op8 = STRING; p = global;
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc] ->
-           let (a8,n8,b) =
-             Metasyntax.interp_infix_modifiers None None modl in
-           VernacInfix (local,None,None,"",p,b,Some(a8,n8,op8),sc)
+           let mv8 = Metasyntax.merge_modifiers None None modl in
+           VernacInfix (local,("",[]),p,Some (op8,mv8),sc)
 
      (* "Print" "Grammar" should be here but is in "command" entry in order 
         to factorize with other "Print"-based vernac entries *)
@@ -376,7 +367,8 @@ GEXTEND Gram
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
-      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ]
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
+      | IDENT "format"; s = STRING -> SetFormat s ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index e39ebc823..b6fe4efa3 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -671,7 +671,10 @@ GEXTEND Gram
 
   syntax:
    [ [ IDENT "Open"; local = locality; IDENT "Scope"; sc = IDENT -> 
-         VernacOpenScope (local,sc)
+         VernacOpenCloseScope (local,true,sc)
+
+     | IDENT "Close"; local = locality; IDENT "Scope"; sc = IDENT -> 
+         VernacOpenCloseScope (local,false,sc)
 
      | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT ->
 	 VernacDelimiters (sc,key)
@@ -682,12 +685,11 @@ GEXTEND Gram
      | IDENT "Arguments"; IDENT "Scope"; qid = global;
          "["; scl = LIST0 opt_scope; "]" -> VernacArgumentsScope (qid,scl)
 
-     | IDENT "Infix"; local = locality; (*a = entry_prec; n = OPT natural; *)
+     | IDENT "Infix"; local = locality;
 	 op = STRING; ":="; p = global; 
          modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ];
 	 sc = OPT [ ":"; sc = IDENT -> sc ] ->
-         let (a,n,b) = Metasyntax.interp_infix_modifiers None None modl in
-         VernacInfix (local,a,n,op,p,b,Some(a,n,op),sc)
+         VernacInfix (local,(op,modl),p,Some(op,modl),sc)
      | IDENT "Notation"; local = locality; s = IDENT; ":="; c = constr;
 	   l = [ "("; IDENT "only"; IDENT "parsing"; ")" -> [SetOnlyParsing]
 	       | -> [] ] ->
@@ -749,7 +751,8 @@ GEXTEND Gram
       | IDENT "right"; IDENT "associativity" -> SetAssoc Gramext.RightA
       | IDENT "no"; IDENT "associativity" -> SetAssoc Gramext.NonA
       | x = IDENT; typ = syntax_extension_type -> SetEntryType (x,typ)
-      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing ] ]
+      | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
+      | IDENT "format"; s = STRING -> SetFormat s ] ]
   ;
   syntax_extension_type:
     [ [ IDENT "ident" -> ETIdent | IDENT "global" -> ETReference
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index af9c3fc76..dc9b2663e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -261,7 +261,7 @@ let vernac_delimiters = Metasyntax.add_delimiters
 let vernac_bind_scope sc cll = 
   List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll
 
-let vernac_open_scope = Symbols.open_scope
+let vernac_open_close_scope = Symbols.open_close_scope
 
 let vernac_arguments_scope qid scl =
   Symbols.declare_arguments_scope (global qid) scl
@@ -1103,10 +1103,9 @@ let interp c = match c with
   | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
-  | VernacOpenScope sc -> vernac_open_scope sc
+  | VernacOpenCloseScope sc -> vernac_open_close_scope sc
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
-  | VernacInfix (local,assoc,n,inf,qid,b,mv8,sc) ->
-      vernac_infix local assoc n inf qid b mv8 sc
+  | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
   | VernacDistfix (local,assoc,n,inf,qid,sc) -> 
       vernac_distfix local assoc n inf qid sc
   | VernacNotation (local,c,infpl,mv8,sc) ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 2838f2589..aa307203f 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -160,14 +160,12 @@ type vernac_expr =
   | VernacDistfix of locality_flag *
       grammar_associativity * precedence * string * reference *
       scope_name option
-  | VernacOpenScope of (locality_flag * scope_name)
+  | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * string
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of reference * scope_name option list
-  | VernacInfix of locality_flag *
-      grammar_associativity * precedence option * string * reference * bool *
-      (grammar_associativity * precedence option* string) option *
-      scope_name option
+  | VernacInfix of locality_flag * (string * syntax_modifier list) *
+      reference * (string * syntax_modifier list) option * scope_name option
   | VernacNotation of
       locality_flag * constr_expr * (string * syntax_modifier list) option *
       (string * syntax_modifier list) option * scope_name option
diff --git a/translate/ppvernacnew.ml b/translate/ppvernacnew.ml
index 5bd322900..aea3bb39f 100644
--- a/translate/ppvernacnew.ml
+++ b/translate/ppvernacnew.ml
@@ -409,6 +409,7 @@ let pr_syntax_modifier = function
   | SetAssoc Gramext.NonA -> str"no associativity"
   | SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
   | SetOnlyParsing -> str"only parsing"
+  | SetFormat s -> str"format " ++ qsnew s
 
 let pr_syntax_modifiers = function
   | [] -> mt()
@@ -540,8 +541,9 @@ let rec pr_vernac = function
       hov 1 (str"Syntax " ++ str u ++ spc() ++
       prlist_with_sep sep_v2 pr_syntax_entry el) ++ 
       str " *)"
-  | VernacOpenScope (local,sc) ->
-      str "Open " ++ pr_locality local ++ str "Scope" ++ spc() ++ str sc
+  | VernacOpenCloseScope (local,opening,sc) ->
+      str (if opening then "Open " else "Close ") ++ pr_locality local ++
+      str "Scope" ++ spc() ++ str sc
   | VernacDelimiters (sc,key) ->
       str"Delimit Scope" ++ spc () ++ str sc ++
       spc() ++ str "with " ++ str key
@@ -552,12 +554,8 @@ let rec pr_vernac = function
       |	None -> str"_"
       |	Some sc -> str sc in 
     str"Arguments Scope" ++ spc() ++ pr_reference q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]"
-  | VernacInfix (local,a,p,s,q,_,ov8,sn) -> (* A Verifier *)
-      let mv8,s = match ov8 with
-        | Some (a,p,s) ->
-	    (match p with None -> [] | Some p -> [SetLevel p])@
-	    (match a with None -> [] | Some a -> [SetAssoc a]),s
-        | None -> [],s in
+  | VernacInfix (local,(s,_),q,ov8,sn) -> (* A Verifier *)
+      let s,mv8 = match ov8 with Some smv8 -> smv8 | None -> (s,[]) in
       hov 0 (hov 0 (str"Infix " ++ pr_locality local
       ++ qsnew s ++ str " :=" ++ spc() ++ pr_reference q) ++
       pr_syntax_modifiers mv8 ++