Support for Local flag in Declare Scope, Undelimit/Delimit Scope, Bind Scope.

This is for use in modules. By default, the behavior is local in
sections and Global is forbidden in sections. By default, the behavior
is global in modules.

3 files changed, 38 insertions, 30 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 1f36b042fe..2e5e11bb09 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1584,7 +1584,7 @@ type scope_command =
   | ScopeDelimRemove
   | ScopeClasses of scope_class list
 
-let load_scope_command_common silently_define_scope_if_undefined _ (_,(scope,o)) =
+let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) =
   let declare_scope_if_needed =
     if silently_define_scope_if_undefined then Notation.declare_scope
     else Notation.ensure_scope in
@@ -1599,7 +1599,7 @@ let load_scope_command_common silently_define_scope_if_undefined _ (_,(scope,o))
 let load_scope_command =
   load_scope_command_common true
 
-let open_scope_command i (_,(scope,o)) =
+let open_scope_command i (_,(local,scope,o)) =
   if Int.equal i 1 then
     match o with
     | ScopeDeclare -> ()
@@ -1611,34 +1611,37 @@ let cache_scope_command o =
   load_scope_command_common false 1 o;
   open_scope_command 1 o
 
-let subst_scope_command (subst,(scope,o as x)) = match o with
+let subst_scope_command (subst,(local,scope,o as x)) = match o with
   | ScopeClasses cl ->
       let cl' = List.map_filter (subst_scope_class subst) cl in
       let cl' =
         if List.for_all2eq (==) cl cl' then cl
         else cl' in
-      scope, ScopeClasses cl'
+      local, scope, ScopeClasses cl'
   | _ -> x
 
-let inScopeCommand : scope_name * scope_command -> obj =
+let classify_scope_command (local, _, _ as o) =
+  if local then Dispose else Substitute o
+
+let inScopeCommand : locality_flag * scope_name * scope_command -> obj =
   declare_object {(default_object "DELIMITERS") with
       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)}
+      classify_function = classify_scope_command}
 
-let declare_scope scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDeclare))
+let declare_scope local scope =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare))
 
-let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimAdd key))
+let add_delimiters local scope key =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key))
 
-let remove_delimiters scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimRemove))
+let remove_delimiters local scope =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove))
 
-let add_class_scope scope cl =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
+let add_class_scope local scope cl =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl))
 
 (* Check if abbreviation to a name and avoid early insertion of
    maximal implicit arguments *)
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 7a74dcfaa9..38dbdf7e41 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -29,10 +29,10 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit
 
 (** Declaring scopes, delimiter keys and default scopes *)
 
-val declare_scope : scope_name -> unit
-val add_delimiters : scope_name -> string -> unit
-val remove_delimiters : scope_name -> unit
-val add_class_scope : scope_name -> scope_class list -> unit
+val declare_scope : locality_flag -> scope_name -> unit
+val add_delimiters : locality_flag -> scope_name -> string -> unit
+val remove_delimiters : locality_flag -> scope_name -> unit
+val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit
 
 (** Add only the interpretation of a notation that already has pa/pp rules *)
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 0fccfd22c6..84ce79d402 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -403,20 +403,24 @@ let dump_global r =
 (**********)
 (* Syntax *)
 
-let vernac_syntax_extension atts infix l =
+let vernac_syntax_extension ~atts infix l =
   let local = enforce_module_locality atts.locality in
   if infix then Metasyntax.check_infix_modifiers (snd l);
   Metasyntax.add_syntax_extension local l
 
-let vernac_declare_scope sc =
-  Metasyntax.declare_scope sc
+let vernac_declare_scope ~atts sc =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.declare_scope local sc
 
-let vernac_delimiters sc = function
-  | Some lr -> Metasyntax.add_delimiters sc lr
-  | None -> Metasyntax.remove_delimiters sc
+let vernac_delimiters ~atts sc action =
+  let local = enforce_module_locality atts.locality in
+  match action with
+  | Some lr -> Metasyntax.add_delimiters local sc lr
+  | None -> Metasyntax.remove_delimiters local sc
 
-let vernac_bind_scope sc cll =
-  Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll)
+let vernac_bind_scope ~atts sc cll =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll)
 
 let vernac_open_close_scope ~atts (b,s) =
   let local = enforce_section_locality atts.locality in
@@ -2096,10 +2100,10 @@ let interp ?proof ~atts ~st c =
 
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-      vernac_syntax_extension atts infix sl
-  | VernacDeclareScope sc -> vernac_declare_scope sc
-  | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
-  | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
+      vernac_syntax_extension ~atts infix sl
+  | VernacDeclareScope sc -> vernac_declare_scope ~atts sc
+  | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr
+  | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
   | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc
   | VernacNotation (c,infpl,sc) ->
@@ -2236,6 +2240,7 @@ let check_vernac_supports_locality c l =
   | Some _, (
       VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+    | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacDeclareCustomEntry _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _