From aac2d2ac490492f8466e1d45ba0079de376fe25a Mon Sep 17 00:00:00 2001
From: Lionel Rieg
Date: Thu, 25 Jun 2015 14:58:25 +0200
Subject: Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"

---
 interp/notation.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'interp/notation.ml')

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 ->
-- 
cgit v1.2.3