diff options
| author |  Lionel Rieg <lionel.rieg@ensiie.fr> | 2015-06-25 14:58:25 +0200 |
|---|---|---|
| committer |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-06-26 11:33:57 +0200 |
| commit | aac2d2ac490492f8466e1d45ba0079de376fe25a (patch) | |
| tree | a7cde3a9f7bf933a912c37a0882813e85b8051b0 /toplevel/metasyntax.ml | |
| parent | e7be889cdc86190ab71709a708e4beb6d3040dd8 (diff) | |
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
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 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)) |