From e0d682ec25282a348d35c5b169abafec48555690 Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Mon, 20 Aug 2012 18:27:01 +0200
Subject: Imported Upstream version 8.4dfsg

---
 interp/notation.ml | 35 ++++++++++++++++++++++++++---------
 1 file changed, 26 insertions(+), 9 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index d2bee550..e3fb5d5e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -53,6 +53,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
@@ -74,12 +77,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                                         *)
 
@@ -99,10 +115,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
@@ -142,8 +161,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
@@ -361,7 +378,7 @@ let interp_prim_token_gen g loc p local_scopes =
   with Not_found ->
     user_err_loc (loc,"interp_prim_token",
     (match p with
-      | Numeral n -> str "No interpretation for numeral " ++ pr_bigint n
+      | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
-- 
cgit v1.2.3