Merge PR #7135: Introducing an explicit `Declare Scope` command

6 files changed, 87 insertions, 38 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74516e320c..44c0159d1b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram
 	 info = hint_info ->
 	   { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) }
 
+      (* Should be in syntax, but camlp5 would not factorize *)
+      | IDENT "Declare"; IDENT "Scope"; sc = IDENT ->
+          { VernacDeclareScope sc }
+
       (* System directory *)
       | IDENT "Pwd" -> { VernacChdir None }
       | IDENT "Cd" -> { VernacChdir None }
@@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram
 	 l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ]
          -> { VernacSyntaxExtension (false, (s,l)) }
 
-     (* "Print" "Grammar" should be here but is in "command" entry in order
-        to factorize with other "Print"-based vernac entries *)
+     (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order
+        to factorize with other "Print"-based or "Declare"-based vernac entries *)
   ] ]
   ;
   only_parsing:
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index d66a121437..2e5e11bb09 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1306,8 +1306,18 @@ type notation_obj = {
   notobj_notation : notation * notation_location;
 }
 
-let load_notation _ (_, nobj) =
-  Option.iter Notation.declare_scope nobj.notobj_scope
+let load_notation_common silently_define_scope_if_undefined _ (_, nobj) =
+  (* When the default shall be to require that a scope already exists *)
+  (* the call to ensure_scope will have to be removed *)
+  if silently_define_scope_if_undefined then
+    (* Don't warn if the scope is not defined: *)
+    (* there was already a warning at "cache" time *)
+    Option.iter Notation.declare_scope nobj.notobj_scope
+  else
+    Option.iter Notation.ensure_scope nobj.notobj_scope
+
+let load_notation =
+  load_notation_common true
 
 let open_notation i (_, nobj) =
   let scope = nobj.notobj_scope in
@@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) =
   end
 
 let cache_notation o =
-  load_notation 1 o;
+  load_notation_common false 1 o;
   open_notation 1 o
 
 let subst_notation (subst, nobj) =
@@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc =
   add_notation local env c (df,modifiers) sc
 
 (**********************************************************************)
-(* Delimiters and classes bound to scopes                             *)
+(* Scopes, delimiters and classes bound to scopes                     *)
 
 type scope_command =
-  | ScopeDelim of string
+  | ScopeDeclare
+  | ScopeDelimAdd of string
+  | ScopeDelimRemove
   | ScopeClasses of scope_class list
-  | ScopeRemove
-
-let load_scope_command _ (_,(scope,dlm)) =
-  Notation.declare_scope scope
 
-let open_scope_command i (_,(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
+  match o with
+  | ScopeDeclare -> Notation.declare_scope scope
+  (* When the default shall be to require that a scope already exists *)
+  (* the call to declare_scope_if_needed will have to be removed below *)
+  | ScopeDelimAdd dlm -> declare_scope_if_needed scope
+  | ScopeDelimRemove -> declare_scope_if_needed scope
+  | ScopeClasses cl -> declare_scope_if_needed scope
+
+let load_scope_command =
+  load_scope_command_common true
+
+let open_scope_command i (_,(local,scope,o)) =
   if Int.equal i 1 then
     match o with
-    | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+    | ScopeDeclare -> ()
+    | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm
+    | ScopeDelimRemove -> Notation.remove_delimiters scope
     | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl
-    | ScopeRemove -> Notation.remove_delimiters scope
 
 let cache_scope_command o =
-  load_scope_command 1 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 local scope =
+  Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare))
 
-let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim 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,ScopeRemove))
+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 73bee7121b..38dbdf7e41 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr ->
 
 val add_notation_extra_printing_rule : string -> string -> string -> unit
 
-(** Declaring delimiter keys and default scopes *)
+(** Declaring scopes, delimiter keys and default scopes *)
 
-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/ppvernac.ml b/vernac/ppvernac.ml
index 93e4e89a12..63e9e4fe49 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -635,6 +635,10 @@ open Pputils
           keyword (if opening then "Open " else "Close ") ++
             keyword "Scope" ++ spc() ++ str sc
         )
+      | VernacDeclareScope sc ->
+        return (
+          keyword "Declare Scope" ++ spc () ++ str sc
+        )
       | VernacDelimiters (sc,Some key) ->
         return (
           keyword "Delimit Scope" ++ spc () ++ str sc ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 385e28f64b..681dce3ca3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -403,17 +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_delimiters sc = function
-  | Some lr -> Metasyntax.add_delimiters sc lr
-  | None -> Metasyntax.remove_delimiters sc
+let vernac_declare_scope ~atts sc =
+  let local = enforce_module_locality atts.locality in
+  Metasyntax.declare_scope local 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
@@ -2093,9 +2100,10 @@ let interp ?proof ~atts ~st c =
 
   (* Syntax *)
   | VernacSyntaxExtension (infix, sl) ->
-      vernac_syntax_extension atts infix sl
-  | 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) ->
@@ -2232,6 +2240,7 @@ let check_vernac_supports_locality c l =
   | Some _, (
       VernacOpenCloseScope _
     | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _
+    | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _
     | VernacDeclareCustomEntry _
     | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _
     | VernacAssumption _ | VernacStartTheoremProof _
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8fb74e6d78..11b2a7d802 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -325,6 +325,7 @@ type nonrec vernac_expr =
   (* Syntax *)
   | VernacSyntaxExtension of bool * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of bool * scope_name
+  | VernacDeclareScope of scope_name
   | VernacDelimiters of scope_name * string option
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacInfix of (lstring * syntax_modifier list) *