diff options
| -rw-r--r-- | vernac/metasyntax.ml | 31 | ||||
| -rw-r--r-- | vernac/metasyntax.mli | 8 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 29 |
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 _ |