# HG changeset patch
# User wenzelm
# Date 1492032942 -7200
# Node ID 5624e9694915e7df8f893382a47d0a2a7455ba34
# Parent  b47373f5245116ebd992440d3e413d6249f2ce80
tuned according to Scala version;

diff -r b47373f52451 -r 5624e9694915 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Wed Apr 12 23:08:24 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Wed Apr 12 23:35:42 2017 +0200
@@ -108,25 +108,26 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
-fun theory_name qualifier theory0 =
+fun loaded_theory_name qualifier theory0 =
   (case loaded_theory theory0 of
     SOME theory => (true, theory)
   | NONE =>
-      (false,
+      let val theory =
         if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
           orelse true (* FIXME *) then theory0
-        else Long_Name.qualify qualifier theory0));
+        else Long_Name.qualify qualifier theory0
+      in (false, theory) end);
 
 fun import_name qualifier dir s =
-  let
-    val (loaded, theory) = theory_name qualifier (Thy_Header.import_name s);
-    val node_name =
-      if loaded then Path.basic theory
-      else
+  (case loaded_theory_name qualifier (Thy_Header.import_name s) of
+    (true, theory) =>
+      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+  | (false, theory) =>
+      let val node_name =
         (case known_theory theory of
           SOME node_name => node_name
-        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))));
-  in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end;
+        | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
+      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
 
 fun check_file dir file = File.check_file (File.full_path dir file);