# HG changeset patch
# User wenzelm
# Date 1491853401 -7200
# Node ID da59e8e0a66316f45c39c81081809625728b58e2
# Parent  cf504b7a7aa7d2eba9baadcfc18f3b69551b502c
clarified theory_long_name (for qualified access to Thy_Info) vs. short theory_name (which is unique within any given theory context);

diff -r cf504b7a7aa7 -r da59e8e0a663 src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Mon Apr 10 21:05:31 2017 +0200
+++ b/src/Pure/Thy/present.ML	Mon Apr 10 21:43:21 2017 +0200
@@ -67,7 +67,7 @@
         val name = Context.theory_name thy;
         val deps = map (node_name o Context.theory_name) (Theory.parents_of thy);
       in
-        if parent_loaded name then NONE
+        if parent_loaded (Context.theory_long_name thy) then NONE
         else SOME ((node_name name, Graph_Display.content_node name []), deps)
       end;
   in
diff -r cf504b7a7aa7 -r da59e8e0a663 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Apr 10 21:05:31 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Apr 10 21:43:21 2017 +0200
@@ -128,8 +128,8 @@
 
 fun update deps theory thys =
   let
-    val name = Context.theory_name theory;
-    val parents = map Context.theory_name (Theory.parents_of theory);
+    val name = Context.theory_long_name theory;
+    val parents = map Context.theory_long_name (Theory.parents_of theory);
 
     val thys' = remove name thys;
     val _ = map (get thys') parents;
@@ -372,7 +372,7 @@
 
 fun register_thy theory =
   let
-    val name = Context.theory_name theory;
+    val name = Context.theory_long_name theory;
     val {master, ...} = Resources.check_thy (Resources.master_directory theory) name;
     val imports = Resources.imports_of theory;
   in
diff -r cf504b7a7aa7 -r da59e8e0a663 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Apr 10 21:05:31 2017 +0200
+++ b/src/Pure/context.ML	Mon Apr 10 21:43:21 2017 +0200
@@ -33,7 +33,9 @@
   val timing: bool Unsynchronized.ref
   val parents_of: theory -> theory list
   val ancestors_of: theory -> theory list
+  val theory_id_long_name: theory_id -> string
   val theory_id_name: theory_id -> string
+  val theory_long_name: theory -> string
   val theory_name: theory -> string
   val PureN: string
   val pretty_thy: theory -> Pretty.T
@@ -148,8 +150,11 @@
 fun make_history name stage = {name = name, stage = stage};
 fun make_ancestry parents ancestors = {parents = parents, ancestors = ancestors};
 
-val theory_id_name = #name o history_of_id;
-val theory_name = #name o history_of;
+val theory_id_long_name = #name o history_of_id;
+val theory_id_name = Long_Name.base_name o theory_id_long_name;
+val theory_long_name = #name o history_of;
+val theory_name = Long_Name.base_name o theory_long_name;
+
 val parents_of = #parents o ancestry_of;
 val ancestors_of = #ancestors o ancestry_of;