Thomas Reichel (Mar 13 2023 at 07:52): Thomas Reichel (Mar 13 2023 at 07:52):Hi all, I know that Locate can look up the full (longest) qualid/path of something in the environment, but I'd also like to be able to Print a term using only full qualids/paths in the output. What would be the easiest way to do this in a plugin? At least under my cursory inspection it doesn't look like it's possible to convince the existing printers to do this. Thanks!
Hugo Herbelin (Mar 14 2023 at 22:23):There is at least a hackish way to do it (I don't how much other devs would be ok to recommend it): it is to use Constrextern.set_extern_reference to set the printer you want (typically Nametab.full_name_cci in place of Nametab.shortest_qualid_of_global, I guess).
Otherwise, we may also add a new option, say Set Printing Fully Qualified. to specifically print references fully qualified in Constrextern.default_extern_reference and make a PR for it.
Last updated: Apr 19 2024 at 13:02 UTC