diff options
-rw-r--r-- | library/nametab.ml | 5 | ||||
-rw-r--r-- | library/nametab.mli | 2 | ||||
-rw-r--r-- | printing/prettyp.ml | 26 | ||||
-rw-r--r-- | printing/prettyp.mli | 1 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 13 |
5 files changed, 29 insertions, 18 deletions
diff --git a/library/nametab.ml b/library/nametab.ml index edceacaa8..3bd4e03ab 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -431,6 +431,8 @@ let locate_extended_all_tactic qid = KnTab.find_prefixes qid !the_tactictab let locate_extended_all_dir qid = DirTab.find_prefixes qid !the_dirtab +let locate_extended_all_modtype qid = MPTab.find_prefixes qid !the_modtypetab + (* Derived functions *) let locate_constant qid = @@ -490,6 +492,9 @@ let dirpath_of_module mp = let path_of_tactic kn = KNmap.find kn !the_tacticrevtab +let path_of_modtype mp = + MPmap.find mp !the_modtyperevtab + (* Shortest qualid functions **********************************************) let shortest_qualid_of_global ctx ref = diff --git a/library/nametab.mli b/library/nametab.mli index 1289a6745..eb2cecc59 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -113,6 +113,7 @@ val locate_all : qualid -> global_reference list val locate_extended_all : qualid -> extended_global_reference list val locate_extended_all_tactic : qualid -> ltac_constant list val locate_extended_all_dir : qualid -> global_dir_reference list +val locate_extended_all_modtype : qualid -> module_path list (** Mapping a full path to a global reference *) @@ -143,6 +144,7 @@ val full_name_module : qualid -> DirPath.t val path_of_syndef : syndef_name -> full_path val path_of_global : global_reference -> full_path val dirpath_of_module : module_path -> DirPath.t +val path_of_modtype : module_path -> full_path val path_of_tactic : ltac_constant -> full_path (** Returns in particular the dirpath or the basename of the full path diff --git a/printing/prettyp.ml b/printing/prettyp.ml index c5840e20b..67b3df35e 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -262,7 +262,7 @@ type logical_name = | Term of global_reference | Dir of global_dir_reference | Syntactic of kernel_name - | ModuleType of qualid * module_path + | ModuleType of module_path | Tactic of Nametab.ltac_constant | Undefined of qualid @@ -274,7 +274,7 @@ let locate_any_name ref = with Not_found -> try Dir (Nametab.locate_dir qid) with Not_found -> - try ModuleType (qid, Nametab.locate_modtype qid) + try ModuleType (Nametab.locate_modtype qid) with Not_found -> Undefined qid let pr_located_qualid = function @@ -296,8 +296,8 @@ let pr_located_qualid = function | DirClosedSection dir -> "Closed Section", dir in str s ++ spc () ++ pr_dirpath dir - | ModuleType (qid,_) -> - str "Module Type" ++ spc () ++ pr_path (Nametab.full_name_modtype qid) + | ModuleType mp -> + str "Module Type" ++ spc () ++ pr_path (Nametab.path_of_modtype mp) | Tactic kn -> str "Ltac" ++ spc () ++ pr_path (Nametab.path_of_tactic kn) | Undefined qid -> @@ -350,10 +350,23 @@ let locate_module qid = in List.map_filter map all +let locate_modtype qid = + let all = Nametab.locate_extended_all_modtype qid in + let map mp = ModuleType mp, Nametab.shortest_qualid_of_modtype mp in + let modtypes = List.map map all in + (** Don't forget the opened module types: they are not part of the same name tab. *) + let all = Nametab.locate_extended_all_dir qid in + let map dir = match dir with + | DirOpenModtype _ -> Some (Dir dir, qid) + | _ -> None + in + modtypes @ List.map_filter map all + let print_located_qualid name flags ref = let (loc,qid) = qualid_of_reference ref in let located = [] in let located = if List.mem `LTAC flags then locate_tactic qid @ located else located in + let located = if List.mem `MODTYPE flags then locate_modtype qid @ located else located in let located = if List.mem `MODULE flags then locate_module qid @ located else located in let located = if List.mem `TERM flags then locate_term qid @ located else located in match located with @@ -375,7 +388,8 @@ let print_located_qualid name flags ref = let print_located_term ref = print_located_qualid "term" [`TERM] ref let print_located_tactic ref = print_located_qualid "tactic" [`LTAC] ref -let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE] ref +let print_located_module ref = print_located_qualid "module" [`MODULE; `MODTYPE] ref +let print_located_qualid ref = print_located_qualid "object" [`TERM; `LTAC; `MODULE; `MODTYPE] ref (******************************************) (**** Printing declarations and judgments *) @@ -662,7 +676,7 @@ let print_any_name = function | Syntactic kn -> print_syntactic_def kn | Dir (DirModule(dirpath,(mp,_))) -> print_module (printable_body dirpath) mp | Dir _ -> mt () - | ModuleType (_,kn) -> print_modtype kn + | ModuleType mp -> print_modtype mp | Tactic kn -> mt () (** TODO *) | Undefined qid -> try (* Var locale de but, pas var de section... donc pas d'implicits *) diff --git a/printing/prettyp.mli b/printing/prettyp.mli index de34131fe..595637745 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -57,6 +57,7 @@ val inspect : int -> std_ppcmds val print_located_qualid : reference -> std_ppcmds val print_located_term : reference -> std_ppcmds val print_located_tactic : reference -> std_ppcmds +val print_located_module : reference -> std_ppcmds type object_pr = { print_inductive : mutual_inductive -> std_ppcmds; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 4141f9f56..4106d29df 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -397,17 +397,6 @@ let print_located_library r = | Library.LibUnmappedDir -> err_unmapped_library loc qid | Library.LibNotFound -> err_notfound_library loc qid -let print_located_module r = - let (loc,qid) = qualid_of_reference r in - try - let dir = Nametab.full_name_module qid in - msg_notice (str "Module " ++ pr_dirpath dir) - with Not_found -> - if DirPath.is_empty (fst (repr_qualid qid)) then - msg_error (str "No module is referred to by basename" ++ spc () ++ pr_qualid qid) - else - msg_error (str "No module is referred to by name" ++ spc () ++ pr_qualid qid) - let smart_global r = let gr = Smartlocate.smart_global r in Dumpglob.add_glob (Constrarg.loc_of_or_by_notation loc_of_reference r) gr; @@ -1540,7 +1529,7 @@ let vernac_locate = function (Notation.locate_notation (Constrextern.without_symbols pr_lglob_constr) ntn sc) | LocateLibrary qid -> print_located_library qid - | LocateModule qid -> print_located_module qid + | LocateModule qid -> msg_notice (print_located_module qid) | LocateTactic qid -> msg_notice (print_located_tactic qid) | LocateFile f -> msg_notice (locate_file f) |