Ajout 'Print Scopes' et 'Bind Scope with classes'

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

5 files changed, 49 insertions, 18 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index afa9226e11..a245a4b635 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1471,6 +1471,7 @@ let xlate_vernac =
 	| PrintTables -> xlate_error "TODO: Print Tables"
         | PrintModuleType _ -> xlate_error "TODO: Print Module Type"
         | PrintModule _ -> xlate_error "TODO: Print Module"
+        | PrintScopes -> xlate_error "TODO: Print Scopes"
         | PrintScope _ -> xlate_error "TODO: Print Scope")
   | VernacBeginSection id ->
       CT_coerce_SECTION_BEGIN_to_COMMAND (CT_section (xlate_ident id))
@@ -1618,6 +1619,8 @@ let xlate_vernac =
 
    | VernacDelimiters _ -> xlate_error "TODO: Delimiters"
 
+   | VernacBindScope _ -> xlate_error "TODO: Bind Scope"
+
    | VernacNotation _ -> xlate_error "TODO: Notation"
 
    | VernacSyntaxExtension _ -> xlate_error "Syntax Extension not implemented"
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 2a5fd697c9..c65d0bc737 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -922,23 +922,39 @@ let add_infix local assoc n inf pr onlyparse mv8 sc =
         Some(split ("x "^quote s8^" y"),(a8,n8,[],false)) in
   add_notation_in_scope local df a (assoc,n,[],onlyparse) mv8 sc (split df)
 
-(* Delimiters *)
-let load_delimiters _ (_,(scope,dlm)) =
+(* Delimiters and classes bound to scopes *)
+type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
+
+let load_scope_command _ (_,(scope,dlm)) =
   Symbols.declare_scope scope
 
-let open_delimiters i (_,(scope,dlm)) =
-  if i=1 then Symbols.declare_delimiters scope dlm
+let open_scope_command i (_,(scope,o)) =
+  if i=1 then
+    match o with
+    | ScopeDelim dlm -> Symbols.declare_delimiters scope dlm
+    | ScopeClasses cl -> Symbols.declare_class_scope scope cl
+
+let cache_scope_command o =
+  load_scope_command 1 o;
+  open_scope_command 1 o
 
-let cache_delimiters o =
-  load_delimiters 1 o;
-  open_delimiters 1 o
+let subst_scope_command (_,subst,(scope,o as x)) = match o with
+  | ScopeClasses cl -> 
+      let cl' = Classops.subst_cl_typ subst cl in if cl'==cl then x else
+      scope, ScopeClasses cl'
+  | _ -> x
 
-let (inDelim,outDelim) = 
+let (inScopeCommand,outScopeCommand) = 
   declare_object {(default_object "DELIMITERS") with
-      cache_function = cache_delimiters;
-      open_function = open_delimiters;
-      load_function = load_delimiters;
+      cache_function = cache_scope_command;
+      open_function = open_scope_command;
+      load_function = load_scope_command;
+      subst_function = subst_scope_command;
+      classify_function = (fun (_,obj) -> Substitute obj);
       export_function = (fun x -> Some x) }
 
 let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inDelim(scope,key))
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
+
+let add_class_scope scope cl = 
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index 31b8e046d0..12aedc600e 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -39,6 +39,7 @@ val translate_distfix : grammar_associativity -> string -> reference ->
   Gramext.g_assoc * string * constr_expr
 
 val add_delimiters : scope_name -> string -> unit
+val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
 val add_notation : locality_flag -> constr_expr
   -> (string * syntax_modifier list) option
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2b3b05b302..f21a9c57e8 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -50,6 +50,13 @@ type pcoq_hook = {
 let pcoq = ref None
 let set_pcoq_hook f = pcoq := Some f
 
+(* Misc *)
+
+let cl_of_qualid = function
+  | FunClass -> Classops.CL_FUN
+  | SortClass -> Classops.CL_SORT
+  | RefClass r -> Class.class_of_ref (Nametab.global r)
+
 (*******************)
 (* "Show" commands *)
 
@@ -300,6 +307,9 @@ let vernac_syntax_extension = Metasyntax.add_syntax_extension
 
 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_arguments_scope qid scl =
@@ -585,11 +595,6 @@ let vernac_import export qidl =
 let vernac_canonical locqid =
   Recordobj.objdef_declare (Nametab.global locqid)
 
-let cl_of_qualid = function
-  | FunClass -> Classops.CL_FUN
-  | SortClass -> Classops.CL_SORT
-  | RefClass r -> Class.class_of_ref (Nametab.global r)
-
 let vernac_coercion stre ref qids qidt =
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
@@ -904,7 +909,10 @@ let vernac_print = function
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
   | PrintHintDb -> Auto.print_searchtable ()
-  | PrintScope s -> pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
+  | PrintScopes ->
+      pp (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm))
+  | PrintScope s ->
+      pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
 
 let global_module r =
   let (loc,qid) = qualid_of_reference r in
@@ -1138,6 +1146,7 @@ let interp c = match c with
   | VernacGrammar (univ,al) -> vernac_grammar univ al
   | 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
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
   | VernacInfix (local,assoc,n,inf,qid,b,mv8,sc) ->
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 4594939470..6cda1af50a 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -51,6 +51,7 @@ type printable =
   | PrintHintGoal
   | PrintHintDbName of string
   | PrintHintDb
+  | PrintScopes
   | PrintScope of string
 
 type searchable =
@@ -160,6 +161,7 @@ type vernac_expr =
       scope_name option
   | VernacOpenScope of (locality_flag * 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 * string * reference * bool *