From ea85f46dc0cc34db149c24bb2da8f3130e191fc1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 11 Sep 2009 17:53:30 +0000
Subject: Generalized the possibility to refer to a global name by a notation
 string in most commands expecting a global name (e.g. 'Print "+"' for an
 infix notation or 'Print "{ _ } + { _ }"' for a misfix notation, possibly
 surrounded by a scope delimiter). Support for such smart globals in VERNAC
 EXTEND to do.

Added a file smartlocate.ml for high-level globalization functions.

Mini-nettoyage metasyntax.ml.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12323 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 08936759dd..58c28149dd 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -536,7 +536,7 @@ let decompose_notation_key s =
     let tok =
       match String.sub s n (pos-n) with
       | "_" -> NonTerminal (id_of_string "_")
-      | s -> Terminal s in
+      | s -> Terminal (drop_simple_quotes s) in
     decomp_ntn (tok::dirs) (pos+1)	  
   in
     decomp_ntn [] 0
@@ -650,15 +650,16 @@ let interp_notation_as_global_reference loc test ntn sc =
       | [] -> error_notation_not_reference loc ntn
       | _ -> error_ambiguous_notation loc ntn
 
-let locate_notation prraw ntn =
+let locate_notation prraw ntn scope =
   let ntns = factorize_entries (browse_notation false ntn !scope_map) in
+  let scopes = Option.fold_right push_scope scope !scope_stack in
   if ntns = [] then
     str "Unknown notation"
   else
     t (str "Notation            " ++
     tab () ++ str "Scope     " ++ tab () ++ fnl () ++ 
     prlist (fun (ntn,l) ->
-      let scope = find_default ntn !scope_stack in
+      let scope = find_default ntn scopes in
       prlist 
 	(fun (sc,r,(_,df)) ->
 	  hov 0 (
-- 
cgit v1.2.3