diff options
Diffstat (limited to 'toplevel')
-rw-r--r-- | toplevel/vernacentries.ml | 44 | ||||
-rw-r--r-- | toplevel/vernacinterp.ml | 9 | ||||
-rw-r--r-- | toplevel/vernacinterp.mli | 2 |
3 files changed, 37 insertions, 18 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 7f584a4b9..780ef6dc3 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -112,11 +112,18 @@ let locate_file f = mSG (hOV 0 [< 'sTR"Can't find file"; 'sPC; 'sTR f; 'sPC; 'sTR"on loadpath"; 'fNL >]) -let locate_id id = +let locate_sp sp = try - mSG [< 'sTR (string_of_path (Nametab.sp_of_id CCI id)); 'fNL >] + let ref = Nametab.locate sp in + mSG + [< 'sTR (string_of_path (sp_of_global (Global.env()) ref)); 'fNL >] with Not_found -> - error ((string_of_id id) ^ " not a defined object") + try + mSG + [< 'sTR (string_of_path (Syntax_def.locate_syntactic_definition sp)); + 'fNL >] + with Not_found -> + error ((string_of_path sp) ^ " not a defined object") let print_loadpath () = let l = get_load_path () in @@ -150,7 +157,7 @@ let _ = let _ = add "Locate" (function - | [VARG_IDENTIFIER id] -> (fun () -> locate_id id) + | [VARG_QUALID sp] -> (fun () -> locate_sp sp) | _ -> bad_vernac_args "Locate") (* For compatibility *) @@ -282,9 +289,9 @@ let _ = add "WriteModule" (function | [VARG_IDENTIFIER id] -> - fun () -> let m = string_of_id id in Library.save_module_to m m + fun () -> let m = string_of_id id in Discharge.save_module_to m m | [VARG_IDENTIFIER id; VARG_STRING f] -> - fun () -> Library.save_module_to (string_of_id id) f + fun () -> Discharge.save_module_to (string_of_id id) f | _ -> bad_vernac_args "WriteModule") let _ = @@ -465,8 +472,7 @@ let _ = (fun id_list () -> List.iter (function - | VARG_IDENTIFIER id -> - let sp = Nametab.sp_of_id CCI id in Global.set_transparent sp + | VARG_CONSTANT sp -> Global.set_transparent sp | _ -> bad_vernac_args "TRANSPARENT") id_list) @@ -475,8 +481,7 @@ let _ = (fun id_list () -> List.iter (function - | VARG_IDENTIFIER id -> - let sp = Nametab.sp_of_id CCI id in Global.set_opaque sp + | VARG_CONSTANT sp -> Global.set_opaque sp | _ -> bad_vernac_args "OPAQUE") id_list) @@ -864,7 +869,13 @@ let _ = let _ = add "SEARCH" (function - | [VARG_IDENTIFIER id] -> (fun () -> print_crible id) + | [VARG_QUALID q] -> + (fun () -> + let ref = + try Nametab.locate q + with Not_found -> + Pretype_errors.error_global_not_found_loc loc q + in search_by_head ref) | _ -> bad_vernac_args "SEARCH") let _ = @@ -1230,20 +1241,17 @@ let _ = let _ = add "INFIX" (function - | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; - VARG_IDENTIFIER pref] -> + | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING inf; VARG_QUALID pref] -> (fun () -> - Metasyntax.add_infix - (Extend.gram_assoc assoc) n inf (string_of_id pref)) + Metasyntax.add_infix (Extend.gram_assoc assoc) n inf pref) | _ -> bad_vernac_args "INFIX") let _ = add "DISTFIX" (function - | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_IDENTIFIER f] -> + | [VARG_AST assoc; VARG_NUMBER n; VARG_STRING s; VARG_QUALID pref] -> (fun () -> - Metasyntax.add_distfix - (Extend.gram_assoc assoc) n s (string_of_id f)) + Metasyntax.add_distfix (Extend.gram_assoc assoc) n s pref) | _ -> bad_vernac_args "DISTFIX") let _ = diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml index 602818ccd..fd41ae5d2 100644 --- a/toplevel/vernacinterp.ml +++ b/toplevel/vernacinterp.ml @@ -24,6 +24,8 @@ type vernac_arg = | VARG_NUMBER of int | VARG_NUMBERLIST of int list | VARG_IDENTIFIER of identifier + | VARG_QUALID of section_path + | VARG_CONSTANT of constant_path | VCALL of string * vernac_arg list | VARG_CONSTR of Coqast.t | VARG_CONSTRLIST of Coqast.t list @@ -77,6 +79,13 @@ let rec cvt_varg ast = VCALL (na,List.map cvt_varg l) | Nvar(_,s) -> VARG_IDENTIFIER (id_of_string s) + | Node(loc,"QUALIDARG",p) -> VARG_QUALID (Astterm.interp_qualid p) + | Node(loc,"QUALIDCONSTARG",p) -> + let q = Astterm.interp_qualid p in + let sp = + try Nametab.locate_constant q + with Not_found -> Pretype_errors.error_global_not_found_loc loc q + in VARG_CONSTANT sp | Str(_,s) -> VARG_STRING s | Num(_,n) -> VARG_NUMBER n | Node(_,"NONE",[]) -> VARG_UNIT diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 0a5ccb9aa..a83e452eb 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -20,6 +20,8 @@ type vernac_arg = | VARG_NUMBER of int | VARG_NUMBERLIST of int list | VARG_IDENTIFIER of identifier + | VARG_QUALID of section_path + | VARG_CONSTANT of constant_path | VCALL of string * vernac_arg list | VARG_CONSTR of Coqast.t | VARG_CONSTRLIST of Coqast.t list |