Adding a command "Declare Scope" and deprecating scope implicit declaration.

9 files changed, 86 insertions, 22 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 55ead946cb..6b26f66100 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -98,21 +98,40 @@ let init_scope_map () =
 (**********************************************************************)
 (* Operations on scopes *)
 
+let warn_undeclared_scope =
+  CWarnings.create ~name:"undeclared-scope" ~category:"deprecated"
+                   (fun (scope) ->
+                    strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit "
+                    ++ str "\"Declare Scope " ++ str scope ++ str ".\".")
+
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
   with Not_found ->
-(*    Flags.if_warn message ("Creating scope "^scope);*)
     scope_map := String.Map.add scope empty_scope !scope_map
 
 let error_unknown_scope sc =
   user_err ~hdr:"Notation"
     (str "Scope " ++ str sc ++ str " is not declared.")
 
-let find_scope scope =
+let find_scope ?(tolerant=false) scope =
   try String.Map.find scope !scope_map
-  with Not_found -> error_unknown_scope scope
+  with Not_found ->
+    if tolerant then
+      (* tolerant mode to be turn off after deprecation phase *)
+      begin
+        warn_undeclared_scope scope;
+        scope_map := String.Map.add scope empty_scope !scope_map;
+        empty_scope
+      end
+    else
+      error_unknown_scope scope
+
+let check_scope ?(tolerant=false) scope =
+  let _ = find_scope ~tolerant scope in ()
+
+let ensure_scope scope = check_scope ~tolerant:true scope
 
-let check_scope sc = let _ = find_scope sc in ()
+let find_scope scope = find_scope scope
 
 (* [sc] might be here a [scope_name] or a [delimiter]
    (now allowed after Open Scope) *)
@@ -418,7 +437,7 @@ type prim_token_infos = {
 let cache_prim_token_interpretation (_,infos) =
   let sc = infos.pt_scope in
   let uid = infos.pt_uid in
-  declare_scope sc;
+  check_scope ~tolerant:true sc;
   prim_token_interp_infos :=
     String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos;
   List.iter (fun r -> prim_token_uninterp_infos :=
diff --git a/interp/notation.mli b/interp/notation.mli
index e5478eff48..6e59c0fd70 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *)
 
 val declare_scope : scope_name -> unit
 
+(* To be removed after deprecation phase *)
+val ensure_scope : scope_name -> unit
+
 val current_scopes : unit -> scopes
 
 (** Check where a scope is opened or not in a scope list, or in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 2170477938..85babd922b 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -168,7 +168,8 @@ let classify_vernac e =
     | VernacDeclareModuleType ({v=id},bl,_,_) ->
         VtSideff [id], if bl = [] then VtLater else VtNow
     (* These commands alter the parser *)
-    | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _
+    | VernacOpenCloseScope _ | VernacDeclareScope _
+    | VernacDelimiters _ | VernacBindScope _
     | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _
     | VernacSyntaxExtension _
     | VernacSyntacticDefinition _
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..1f36b042fe 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,25 +1576,39 @@ 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 load_scope_command_common silently_define_scope_if_undefined _ (_,(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 (_,(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
@@ -1604,11 +1628,14 @@ let inScopeCommand : scope_name * scope_command -> obj =
       subst_function = subst_scope_command;
       classify_function = (fun obj -> Substitute obj)}
 
+let declare_scope scope =
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDeclare))
+
 let add_delimiters scope key =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key))
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimAdd key))
 
 let remove_delimiters scope =
-  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove))
+  Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelimRemove))
 
 let add_class_scope scope cl =
   Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl))
diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli
index 73bee7121b..7a74dcfaa9 100644
--- a/vernac/metasyntax.mli
+++ b/vernac/metasyntax.mli
@@ -27,8 +27,9 @@ 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 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
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 f7ba305374..0fccfd22c6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -408,6 +408,9 @@ let vernac_syntax_extension atts infix l =
   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_delimiters sc = function
   | Some lr -> Metasyntax.add_delimiters sc lr
   | None -> Metasyntax.remove_delimiters sc
@@ -2094,6 +2097,7 @@ 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
   | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s)
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) *