From 3b7a6761f5c9bf5026c4517e8032aa4384185528 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 29 Mar 2018 20:07:34 +0200
Subject: Adding a command "Declare Scope" and deprecating scope implicit
 declaration.

---
 vernac/g_vernac.mlg     |  8 ++++++--
 vernac/metasyntax.ml    | 53 +++++++++++++++++++++++++++++++++++++------------
 vernac/metasyntax.mli   |  3 ++-
 vernac/ppvernac.ml      |  4 ++++
 vernac/vernacentries.ml |  4 ++++
 vernac/vernacexpr.ml    |  1 +
 6 files changed, 57 insertions(+), 16 deletions(-)

(limited to 'vernac')

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) *
-- 
cgit v1.2.3


From 8e675d70ad1f60cbbf9f1e630ce6dee61347c7ca Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 30 Jul 2018 12:32:35 +0200
Subject: 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.
---
 vernac/metasyntax.ml    | 31 +++++++++++++++++--------------
 vernac/metasyntax.mli   |  8 ++++----
 vernac/vernacentries.ml | 29 +++++++++++++++++------------
 3 files changed, 38 insertions(+), 30 deletions(-)

(limited to 'vernac')

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 _
-- 
cgit v1.2.3