Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"

2 files changed, 14 insertions, 0 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index 555dfa804b..0b5791d32b 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -200,6 +200,19 @@ let declare_delimiters scope key =
     end
   with Not_found -> delimiters_map := String.Map.add key scope !delimiters_map
 
+let remove_delimiters scope =
+  let sc = find_scope scope in
+  let newsc = { sc with delimiters = None } in
+  match sc.delimiters with
+    | None -> msg_warning (str "No bound key for scope " ++ str scope ++ str ".")
+    | Some key ->
+       scope_map := String.Map.add scope newsc !scope_map;
+       try
+         let _ = ignore (String.Map.find key !delimiters_map) in
+         delimiters_map := String.Map.remove key !delimiters_map
+       with Not_found ->
+         assert false (* A delimiter for scope [scope] should exist *)
+
 let find_delimiters_scope loc key =
   try String.Map.find key !delimiters_map
   with Not_found ->
diff --git a/interp/notation.mli b/interp/notation.mli
index 854c52b2c7..38bd5fc7b8 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -55,6 +55,7 @@ val find_scope : scope_name -> scope
 (** Declare delimiters for printing *)
 
 val declare_delimiters : scope_name -> delimiters -> unit
+val remove_delimiters : scope_name -> unit
 val find_delimiters_scope : Loc.t -> delimiters -> scope_name
 
 (** {6 Declare and uses back and forth an interpretation of primitive token } *)