diff options
| author | herbelin | 2009-09-11 17:53:30 +0000 |
|---|---|---|
| committer | herbelin | 2009-09-11 17:53:30 +0000 |
| commit | ea85f46dc0cc34db149c24bb2da8f3130e191fc1 (patch) | |
| tree | 3b8fa67f3f1dc5bb2815b38c1040a3ea192c88fe /interp/notation.ml | |
| parent | 7131609a82198080421b15e2c7a0d8f3b6cbd3de (diff) | |
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
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 7 |
1 files changed, 4 insertions, 3 deletions
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 ( |