# HG changeset patch
# User wenzelm
# Date 1492796633 -7200
# Node ID 6a00518bbfccf6709200c081d0035b367890eaac
# Parent  ae09b9f5980bc6c1a81481457935aa2607e705f2
clarified standard_import: based on Known.get_file as in PIDE editors;

diff -r ae09b9f5980b -r 6a00518bbfcc src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 18:57:30 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 19:43:53 2017 +0200
@@ -80,13 +80,17 @@
       def standard_import(qualifier: String, dir: String, s: String): String =
       {
         val name = imports_resources.import_name(qualifier, dir, s)
+        val file = Path.explode(name.node).file
         val s1 =
-          if (!local_theories.contains(name)) s
-          else if (session_resources.theory_qualifier(name) != qualifier) name.theory
-          else if (Thy_Header.is_base_name(s)) name.theory_base_name
-          else s
-        val name1 = imports_resources.import_name(qualifier, dir, s1)
-        if (name == name1) s1 else s
+          imports_resources.session_base.known.get_file(file) match {
+            case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+              name1.theory
+            case Some(name1) if Thy_Header.is_base_name(s) =>
+              name1.theory_base_name
+            case _ => s
+          }
+        val name2 = imports_resources.import_name(qualifier, dir, s1)
+        if (name.node == name2.node) s1 else s
       }
 
       val updates_root =