--- a/src/Pure/General/name_space.ML Fri May 05 11:52:53 2023 +0200
+++ b/src/Pure/General/name_space.ML Fri May 05 12:01:09 2023 +0200
@@ -23,7 +23,7 @@
val markup_def: T -> string -> Markup.T
val get_names: T -> string list
val the_entry: T -> string -> entry
- val the_entry_theory_name: T -> string -> string
+ val theory_name: {long: bool} -> T -> string -> string
val entry_ord: T -> string ord
val is_concealed: T -> string -> bool
val intern: T -> xstring -> string
@@ -260,8 +260,9 @@
NONE => error (undefined space name)
| SOME entry => entry);
-fun the_entry_theory_name space name =
- Long_Name.base_name (#theory_long_name (the_entry space name));
+fun theory_name {long} space name =
+ #theory_long_name (the_entry space name)
+ |> not long ? Long_Name.base_name;
fun entry_ord space = int_ord o apply2 (#serial o the_entry space);
--- a/src/Tools/Code/code_symbol.ML Fri May 05 11:52:53 2023 +0200
+++ b/src/Tools/Code/code_symbol.ML Fri May 05 12:01:09 2023 +0200
@@ -97,8 +97,9 @@
end;
local
- val thyname_of_type = Name_Space.the_entry_theory_name o Sign.type_space;
- val thyname_of_class = Name_Space.the_entry_theory_name o Sign.class_space;
+ val thyname_of = Name_Space.theory_name {long = false};
+ val thyname_of_type = thyname_of o Sign.type_space;
+ val thyname_of_class = thyname_of o Sign.class_space;
fun thyname_of_instance thy inst = case Thm.theory_names_of_arity {long = false} thy inst
of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^ snd inst))
| thyname :: _ => thyname;
@@ -106,7 +107,7 @@
of SOME class => thyname_of_class thy class
| NONE => (case Code.get_type_of_constr_or_abstr thy c
of SOME (tyco, _) => thyname_of_type thy tyco
- | NONE => Name_Space.the_entry_theory_name (Sign.const_space thy) c);
+ | NONE => thyname_of (Sign.const_space thy) c);
fun prefix thy (Constant "") = "Code"
| prefix thy (Constant c) = thyname_of_const thy c
| prefix thy (Type_Constructor tyco) = thyname_of_type thy tyco