diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 9 | ||||
| -rw-r--r-- | toplevel/metasyntax.mli | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 4 |
3 files changed, 12 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 300bf5b49..7616bfff6 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1383,7 +1383,10 @@ let add_infix local ((loc,inf),modifiers) pr sc = (**********************************************************************) (* Delimiters and classes bound to scopes *) -type scope_command = ScopeDelim of string | ScopeClasses of scope_class list +type scope_command = + | ScopeDelim of string + | ScopeClasses of scope_class list + | ScopeRemove let load_scope_command _ (_,(scope,dlm)) = Notation.declare_scope scope @@ -1393,6 +1396,7 @@ let open_scope_command i (_,(scope,o)) = match o with | ScopeDelim dlm -> Notation.declare_delimiters scope dlm | 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; @@ -1418,6 +1422,9 @@ let inScopeCommand : scope_name * scope_command -> obj = let add_delimiters scope key = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let remove_delimiters scope = + Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) + let add_class_scope scope cl = Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 38a377577..f22839f48 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -39,6 +39,7 @@ val add_notation_extra_printing_rule : string -> string -> string -> unit (** Declaring 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 (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 8d9f8f52c..04d572cd3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -424,7 +424,9 @@ let vernac_syntax_extension locality local = let local = enforce_module_locality locality local in Metasyntax.add_syntax_extension local -let vernac_delimiters = Metasyntax.add_delimiters +let vernac_delimiters sc = function + | Some lr -> Metasyntax.add_delimiters sc lr + | None -> Metasyntax.remove_delimiters sc let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) |