# HG changeset patch
# User wenzelm
# Date 1491679699 -7200
# Node ID dccbfc715904a8ebbd7c3a9799f48060c8a2229a
# Parent  1ca6d8a2a00dc5b5d8692aad8e9df85802b39c5a
provide Resources.import_name in ML, similar to Scala version;
reset default_qualifier for now;
tuned;

diff -r 1ca6d8a2a00d -r dccbfc715904 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Sat Apr 08 21:09:34 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Sat Apr 08 21:28:19 2017 +0200
@@ -19,6 +19,7 @@
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
+  val import_name: Path.T -> Path.T -> {node_name: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -98,6 +99,21 @@
 
 val thy_path = Path.ext "thy";
 
+fun import_name dir path =
+  let
+    val theory0 = Path.implode (Path.base path);
+    val theory =
+      if Long_Name.is_qualified theory0 orelse global_theory theory0 then theory0
+      else Long_Name.qualify (default_qualifier ()) theory0;
+    val node_name =
+      the (get_first (fn e => e ())
+        [fn () => loaded_theory theory,
+         fn () => loaded_theory theory0,
+         fn () => known_theory theory,
+         fn () => known_theory theory0,
+         fn () => SOME (File.full_path dir (thy_path path))])
+  in {node_name = node_name, theory_name = theory} end;
+
 fun check_file dir file = File.check_file (File.full_path dir file);
 
 fun check_thy dir thy_name =
diff -r 1ca6d8a2a00d -r dccbfc715904 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:09:34 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Sat Apr 08 21:28:19 2017 +0200
@@ -291,39 +291,38 @@
 and require_thy document symbols last_timing initiators dir (str, require_pos) tasks =
   let
     val path = Path.expand (Path.explode str);
-    val name = Path.implode (Path.base path);
-    val node_name = File.full_path dir (Resources.thy_path path);
+    val {node_name, theory_name} = Resources.import_name dir path;
     fun check_entry (Task (node_name', _, _)) =
           if op = (apply2 File.platform_path (node_name, node_name'))
           then ()
           else
-            error ("Incoherent imports for theory " ^ quote name ^
+            error ("Incoherent imports for theory " ^ quote theory_name ^
               Position.here require_pos ^ ":\n" ^
               "  " ^ Path.print node_name ^ "\n" ^
               "  " ^ Path.print node_name')
       | check_entry _ = ();
   in
-    (case try (String_Graph.get_node tasks) name of
+    (case try (String_Graph.get_node tasks) theory_name of
       SOME task => (check_entry task; (task_finished task, tasks))
     | NONE =>
         let
           val dir' = Path.append dir (Path.dir path);
-          val _ = member (op =) initiators name andalso error (cycle_msg initiators);
+          val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
 
-          val (current, deps, theory_pos, imports, keywords) = check_deps dir' name
+          val (current, deps, theory_pos, imports, keywords) = check_deps dir' theory_name
             handle ERROR msg =>
               cat_error msg
-                ("The error(s) above occurred for theory " ^ quote name ^
+                ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
           val parents = map (base_name o #1) imports;
           val (parents_current, tasks') =
-            require_thys document symbols last_timing (name :: initiators)
+            require_thys document symbols last_timing (theory_name :: initiators)
               (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
-            if all_current then Finished (get_theory name)
+            if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
@@ -332,10 +331,10 @@
                     val update_time = serial ();
                     val load =
                       load_thy document symbols last_timing initiators update_time dep
-                        text (name, theory_pos) keywords;
+                        text (theory_name, theory_pos) keywords;
                   in Task (node_name, parents, load) end);
 
-          val tasks'' = new_entry name parents task tasks';
+          val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;
 
diff -r 1ca6d8a2a00d -r dccbfc715904 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Sat Apr 08 21:09:34 2017 +0200
+++ b/src/Pure/Tools/build.ML	Sat Apr 08 21:28:19 2017 +0200
@@ -180,7 +180,7 @@
 
     val _ =
       Resources.set_session_base
-        {default_qualifier = name,
+        {default_qualifier = "" (* FIXME *),
          global_theories = global_theories,
          loaded_theories = loaded_theories,
          known_theories = known_theories};