diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 44 |
1 files changed, 34 insertions, 10 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 3a162ce7e..d0734b3d8 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -446,19 +446,37 @@ let rec compute_arguments_scope t = let arguments_scope = ref Refmap.empty -let load_arguments_scope _ (_,(r,scl)) = +type arguments_scope_request = + | ArgsScopeAuto + | ArgsScopeManual of bool + +let load_arguments_scope _ (_,(_,r,scl)) = List.iter (option_iter check_scope) scl; arguments_scope := Refmap.add r scl !arguments_scope let cache_arguments_scope o = load_arguments_scope 1 o -let subst_arguments_scope (_,subst,(r,scl)) = (fst (subst_global subst r),scl) - -let discharge_arguments_scope (r,_) = - match r with - | VarRef _ -> None - | _ -> Some (r,compute_arguments_scope (Global.type_of_global r)) +let subst_arguments_scope (_,subst,(req,r,scl)) = + (None,fst (subst_global subst r),scl) + +let discharge_arguments_scope (_,(req,r,l)) = + match req,r with + | _, VarRef _ -> None + | Some (ArgsScopeManual true),_ -> None + | _ -> Some (req,pop_global_reference r,l) + +let rebuild_arguments_scope (req,r,l) = + match req with + | None | Some (ArgsScopeManual true) -> assert false + | Some ArgsScopeAuto -> + (req,r,compute_arguments_scope (Global.type_of_global r)) + | Some (ArgsScopeManual false) -> + (* Add to the manually given scopes the one found automatically + for the extra parameters of the section *) + let l' = compute_arguments_scope (Global.type_of_global r) in + let l1,_ = list_chop (List.length l' - List.length l) l' in + (req,r,l1@l) let (inArgumentsScope,outArgumentsScope) = declare_object {(default_object "ARGUMENTS-SCOPE") with @@ -466,10 +484,15 @@ let (inArgumentsScope,outArgumentsScope) = load_function = load_arguments_scope; subst_function = subst_arguments_scope; classify_function = (fun (_,o) -> Substitute o); + discharge_function = discharge_arguments_scope; + rebuild_function = rebuild_arguments_scope; export_function = (fun x -> Some x) } -let declare_arguments_scope r scl = - Lib.add_anonymous_leaf (inArgumentsScope (r,scl)) +let declare_arguments_scope_gen req r scl = + Lib.add_anonymous_leaf (inArgumentsScope (req,r,scl)) + +let declare_arguments_scope local r scl = + declare_arguments_scope_gen (Some (ArgsScopeManual local)) r scl let find_arguments_scope r = try Refmap.find r !arguments_scope @@ -477,7 +500,8 @@ let find_arguments_scope r = let declare_ref_arguments_scope ref = let t = Global.type_of_global ref in - declare_arguments_scope ref (compute_arguments_scope t) + declare_arguments_scope_gen (Some ArgsScopeAuto) ref + (compute_arguments_scope t) (********************************) (* Encoding notations as string *) |