diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-28 17:10:21 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-28 17:10:21 +0200 |
| commit | 6f982439294b9b53150c6c5d2fd1025e58d7bcd9 (patch) | |
| tree | debf9e53d93b722a871364e06763ddc8b0413bcf /toplevel/metasyntax.ml | |
| parent | 53dc6613499ca18672cda02697f182eb97cda8dc (diff) | |
| parent | 02663c526a3fd347fad803eb664d22e6b5c088ad (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 98b322af1..9864182a0 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1385,7 +1385,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 @@ -1395,6 +1398,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; @@ -1420,6 +1424,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)) |