# HG changeset patch
# User wenzelm
# Date 1575886654 -3600
# Node ID b1f3e86a4745d72b7a2f1ba0a6c16e84a51a4f5f
# Parent  dd74e0558fd17b8babd01a3e6f6b247b8b800025
clarified signature: store full theory name;

diff -r dd74e0558fd1 -r b1f3e86a4745 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Sun Dec 08 17:42:58 2019 +0100
+++ b/src/Pure/General/name_space.ML	Mon Dec 09 11:17:34 2019 +0100
@@ -15,7 +15,12 @@
   val markup: T -> string -> Markup.T
   val markup_def: T -> string -> Markup.T
   val the_entry: T -> string ->
-    {concealed: bool, group: serial option, theory_name: string, pos: Position.T, serial: serial}
+   {concealed: bool,
+    group: serial option,
+    theory_long_name: string,
+    pos: Position.T,
+    serial: serial}
+  val the_entry_theory_name: T -> string -> string
   val entry_ord: T -> string ord
   val is_concealed: T -> string -> bool
   val intern: T -> xstring -> string
@@ -41,7 +46,7 @@
   val concealed: naming -> naming
   val get_group: naming -> serial option
   val set_group: serial option -> naming -> naming
-  val set_theory_name: string -> naming -> naming
+  val set_theory_long_name: string -> naming -> naming
   val new_group: naming -> naming
   val reset_group: naming -> naming
   val add_path: string -> naming -> naming
@@ -102,7 +107,7 @@
 type entry =
  {concealed: bool,
   group: serial option,
-  theory_name: string,
+  theory_long_name: string,
   pos: Position.T,
   serial: serial};
 
@@ -182,6 +187,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 entry_ord space = int_ord o apply2 (#serial o the_entry space);
 
 fun is_concealed space name =
@@ -317,15 +325,15 @@
   restricted: (bool * Binding.scope) option,
   concealed: bool,
   group: serial option,
-  theory_name: string,
+  theory_long_name: string,
   path: (string * bool) list};
 
-fun make_naming (scopes, restricted, concealed, group, theory_name, path) =
+fun make_naming (scopes, restricted, concealed, group, theory_long_name, path) =
   Naming {scopes = scopes, restricted = restricted, concealed = concealed,
-    group = group, theory_name = theory_name, path = path};
+    group = group, theory_long_name = theory_long_name, path = path};
 
-fun map_naming f (Naming {scopes, restricted, concealed, group, theory_name, path}) =
-  make_naming (f (scopes, restricted, concealed, group, theory_name, path));
+fun map_naming f (Naming {scopes, restricted, concealed, group, theory_long_name, path}) =
+  make_naming (f (scopes, restricted, concealed, group, theory_long_name, path));
 
 
 (* scope and access restriction *)
@@ -337,13 +345,13 @@
   let
     val scope = Binding.new_scope ();
     val naming' =
-      naming |> map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
-        (scope :: scopes, restricted, concealed, group, theory_name, path));
+      naming |> map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) =>
+        (scope :: scopes, restricted, concealed, group, theory_long_name, path));
   in (scope, naming') end;
 
 fun restricted_scope strict scope =
-  map_naming (fn (scopes, _, concealed, group, theory_name, path) =>
-    (scopes, SOME (strict, scope), concealed, group, theory_name, path));
+  map_naming (fn (scopes, _, concealed, group, theory_long_name, path) =>
+    (scopes, SOME (strict, scope), concealed, group, theory_long_name, path));
 
 fun restricted strict pos naming =
   (case get_scope naming of
@@ -356,19 +364,21 @@
 val qualified_scope = restricted_scope false;
 val qualified = restricted false;
 
-val concealed = map_naming (fn (scopes, restricted, _, group, theory_name, path) =>
-  (scopes, restricted, true, group, theory_name, path));
+val concealed = map_naming (fn (scopes, restricted, _, group, theory_long_name, path) =>
+  (scopes, restricted, true, group, theory_long_name, path));
 
 
 (* additional structural info *)
 
-fun set_theory_name theory_name = map_naming (fn (scopes, restricted, concealed, group, _, path) =>
-  (scopes, restricted, concealed, group, theory_name, path));
+fun set_theory_long_name theory_long_name =
+  map_naming (fn (scopes, restricted, concealed, group, _, path) =>
+    (scopes, restricted, concealed, group, theory_long_name, path));
 
 fun get_group (Naming {group, ...}) = group;
 
-fun set_group group = map_naming (fn (scopes, restricted, concealed, _, theory_name, path) =>
-  (scopes, restricted, concealed, group, theory_name, path));
+fun set_group group =
+  map_naming (fn (scopes, restricted, concealed, _, theory_long_name, path) =>
+    (scopes, restricted, concealed, group, theory_long_name, path));
 
 fun new_group naming = set_group (SOME (serial ())) naming;
 val reset_group = set_group NONE;
@@ -378,8 +388,9 @@
 
 fun get_path (Naming {path, ...}) = path;
 
-fun map_path f = map_naming (fn (scopes, restricted, concealed, group, theory_name, path) =>
-  (scopes, restricted, concealed, group, theory_name, f path));
+fun map_path f =
+  map_naming (fn (scopes, restricted, concealed, group, theory_long_name, path) =>
+    (scopes, restricted, concealed, group, theory_long_name, f path));
 
 fun add_path elems = map_path (fn path => path @ [(elems, false)]);
 val root_path = map_path (fn _ => []);
@@ -502,7 +513,7 @@
 fun declare context strict binding space =
   let
     val naming = naming_of context;
-    val Naming {group, theory_name, ...} = naming;
+    val Naming {group, theory_long_name, ...} = naming;
     val {concealed, spec, ...} = name_spec naming binding;
     val accesses = make_accesses naming binding;
 
@@ -513,7 +524,7 @@
     val entry =
      {concealed = concealed,
       group = group,
-      theory_name = theory_name,
+      theory_long_name = theory_long_name,
       pos = pos,
       serial = serial ()};
     val space' =
diff -r dd74e0558fd1 -r b1f3e86a4745 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Dec 08 17:42:58 2019 +0100
+++ b/src/Pure/sign.ML	Mon Dec 09 11:17:34 2019 +0100
@@ -525,7 +525,8 @@
 
 fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
 
-fun theory_naming thy = thy |> map_naming (Name_Space.set_theory_name (Context.theory_name thy));
+fun theory_naming thy = thy
+  |> map_naming (Name_Space.set_theory_long_name (Context.theory_long_name thy));
 
 val private_scope = map_naming o Name_Space.private_scope;
 val private = map_naming o Name_Space.private;
diff -r dd74e0558fd1 -r b1f3e86a4745 src/Tools/Code/code_symbol.ML
--- a/src/Tools/Code/code_symbol.ML	Sun Dec 08 17:42:58 2019 +0100
+++ b/src/Tools/Code/code_symbol.ML	Mon Dec 09 11:17:34 2019 +0100
@@ -97,8 +97,8 @@
 end;
 
 local
-  fun thyname_of_type thy = #theory_name o Name_Space.the_entry (Sign.type_space thy);
-  fun thyname_of_class thy = #theory_name o Name_Space.the_entry (Sign.class_space thy);
+  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;
   fun thyname_of_instance thy inst = case Thm.thynames_of_arity thy inst
    of [] => error ("No such instance: " ^ quote (fst inst ^ " :: " ^  snd inst))
     | thyname :: _ => thyname;
@@ -106,7 +106,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 => #theory_name (Name_Space.the_entry (Sign.const_space thy) c));
+        | NONE => Name_Space.the_entry_theory_name (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