diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 21 |
1 files changed, 20 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1d25bc1d9..4e63b16fa 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -670,8 +670,27 @@ let check_no_explicitation l = | (_, Some (loc, _)) :: _ -> user_err_loc (loc,"",str"Unexpected explicitation of the argument of an abbreviation.") +(* This code is taken from dumpglob, and should be shared with it *) +let feedback_global loc ref = + if !Flags.ide_slave then + let remove_sections dir = + if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + else + dir in + let sp = Nametab.path_of_global ref in + let lib_dp = Lib.library_part ref in + let ty = "" in + let mod_dp,id = Libnames.repr_path sp in + let mod_dp = remove_sections mod_dp in + let mod_dp_trunc = Libnames.drop_dirpath_prefix lib_dp mod_dp in + let filepath = Names.DirPath.to_string lib_dp in + let modpath = Names.DirPath.to_string mod_dp_trunc in + let ident = Names.Id.to_string id in + Pp.feedback (Interface.GlobRef (loc, filepath, modpath, ident, ty)) + let dump_extended_global loc = function - | TrueGlobal ref -> Dumpglob.add_glob loc ref + | TrueGlobal ref -> feedback_global loc ref; Dumpglob.add_glob loc ref | SynDef sp -> Dumpglob.add_glob_kn loc sp let intern_extended_global_of_qualid (loc,qid) = |