Open Scope can now also accepts delimiters (e.g. Z).

Of course, scope names (e.g. Z_scope) are still accepted.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15516 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 24 insertions, 7 deletions

diff --git a/interp/notation.ml b/interp/notation.ml
index e42bd787c1..b93ad6bcc4 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -57,6 +57,9 @@ let notation_level_map = ref Gmap.empty
 (* Scopes table: scope_name -> symbol_interpretation *)
 let scope_map = ref Gmap.empty
 
+(* Delimiter table : delimiter -> scope_name *)
+let delimiters_map = ref Gmap.empty
+
 let empty_scope = {
   notations = Gmap.empty;
   delimiters = None
@@ -78,12 +81,25 @@ let declare_scope scope =
 (*    Flags.if_warn message ("Creating scope "^scope);*)
     scope_map := Gmap.add scope empty_scope !scope_map
 
+let error_unknown_scope sc = error ("Scope "^sc^" is not declared.")
+
 let find_scope scope =
   try Gmap.find scope !scope_map
-  with Not_found -> error ("Scope "^scope^" is not declared.")
+  with Not_found -> error_unknown_scope scope
 
 let check_scope sc = let _ = find_scope sc in ()
 
+(* [sc] might be here a [scope_name] or a [delimiter]
+   (now allowed after Open Scope) *)
+
+let normalize_scope sc =
+  try let _ = Gmap.find sc !scope_map in sc
+  with Not_found ->
+    try
+      let sc = Gmap.find sc !delimiters_map in
+      let _ = Gmap.find sc !scope_map in sc
+    with Not_found -> error_unknown_scope sc
+
 (**********************************************************************)
 (* The global stack of scopes                                         *)
 
@@ -103,10 +119,13 @@ let scope_is_open sc = scope_is_open_in_scopes sc (!scope_stack)
 
 (* Exportation of scopes *)
 let open_scope i (_,(local,op,sc)) =
-  if i=1 then begin
-  (match sc with Scope sc -> check_scope sc | _ -> ());
-  scope_stack := if op then sc :: !scope_stack else list_except sc !scope_stack
-  end
+  if i=1 then
+    let sc = match sc with
+      | Scope sc -> Scope (normalize_scope sc)
+      | _ -> sc
+    in
+    scope_stack :=
+      if op then sc :: !scope_stack else list_except sc !scope_stack
 
 let cache_scope o =
   open_scope 1 o
@@ -146,8 +165,6 @@ let make_current_scopes (tmp_scope,scopes) =
 (**********************************************************************)
 (* Delimiters *)
 
-let delimiters_map = ref Gmap.empty
-
 let declare_delimiters scope key =
   let sc = find_scope scope in
   let newsc = { sc with delimiters = Some key } in