# HG changeset patch
# User wenzelm
# Date 1506592435 -7200
# Node ID 80fa1401cf76ba1f14c2144253b8485f1bb7e277
# Parent  0b9e6ce3b843372e636b25752d0c240164d66215
discontinued extra checks (see ce676a750575 and 60c159d490a2) -- qualified theory names are meant to cover this;

diff -r 0b9e6ce3b843 -r 80fa1401cf76 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Thu Sep 28 09:42:28 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
@@ -20,8 +20,7 @@
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
-  val import_name: string -> Path.T -> string ->
-    {node_name: Path.T, master_dir: Path.T, theory_name: string}
+  val import_name: string -> Path.T -> string -> {master_dir: 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}
@@ -120,14 +119,13 @@
 
 fun import_name qualifier dir s =
   (case theory_name qualifier (Thy_Header.import_name s) of
-    (true, theory) =>
-      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+    (true, 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);
+      in {master_dir = Path.dir node_name, theory_name = theory} end);
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
diff -r 0b9e6ce3b843 -r 80fa1401cf76 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Thu Sep 28 09:42:28 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Thu Sep 28 11:53:55 2017 +0200
@@ -160,7 +160,7 @@
   in res :: map Exn.Exn exns end;
 
 datatype task =
-  Task of Path.T * string list * (theory list -> result) |
+  Task of string list * (theory list -> result) |
   Finished of theory;
 
 fun task_finished (Task _) = false
@@ -171,7 +171,7 @@
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
-      Task (_, parents, body) =>
+      Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
@@ -185,7 +185,7 @@
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
-          Task (_, parents, body) =>
+          Task (parents, body) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = NONE,
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
@@ -335,19 +335,10 @@
       |>> forall I
 and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   let
-    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
-    fun check_entry (Task (node_name', _, _)) =
-          if op = (apply2 File.platform_path (node_name, node_name'))
-          then ()
-          else
-            error ("Incoherent imports for theory " ^ quote theory_name ^
-              Position.here require_pos ^ ":\n" ^
-              "  " ^ Path.print node_name ^ "\n" ^
-              "  " ^ Path.print node_name')
-      | check_entry _ = ();
+    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
     (case try (String_Graph.get_node tasks) theory_name of
-      SOME task => (check_entry task; (task_finished task, tasks))
+      SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
@@ -378,7 +369,7 @@
                     val load =
                       load_thy document symbols last_timing initiators update_time dep
                         text (theory_name, theory_pos) keywords;
-                  in Task (node_name, parents, load) end);
+                  in Task (parents, load) end);
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
diff -r 0b9e6ce3b843 -r 80fa1401cf76 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Thu Sep 28 09:42:28 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Thu Sep 28 11:53:55 2017 +0200
@@ -38,44 +38,25 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
+    val empty = new Dependencies(Nil, Nil, Nil, Set.empty)
   }
 
   final class Dependencies private(
     rev_deps: List[Thy_Info.Dep],
     val keywords: Thy_Header.Keywords,
     val abbrevs: Thy_Header.Abbrevs,
-    val seen: Set[Document.Node.Name],
-    val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
+    val seen: Set[Document.Node.Name])
   {
     def :: (dep: Thy_Info.Dep): Dependencies =
       new Dependencies(
-        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
-        seen, seen_theory)
+        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs, seen)
 
-    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
-    {
-      val (name, _) = thy
-      new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
-    }
+    def + (name: Document.Node.Name): Dependencies =
+      new Dependencies(rev_deps, keywords, abbrevs, seen + name)
 
     def deps: List[Thy_Info.Dep] = rev_deps.reverse
 
-    def errors: List[String] =
-    {
-      val header_errors = deps.flatMap(dep => dep.header.errors)
-      val import_errors =
-        (for {
-          (theory, imports) <- seen_theory.iterator_list
-          if !resources.session_base.loaded_theories.isDefinedAt(theory)
-          if imports.length > 1
-        } yield {
-          "Incoherent imports for theory " + quote(theory) + ":\n" +
-            cat_lines(imports.map({ case (name, pos) =>
-              "  " + quote(name.node) + Position.here(pos) }))
-        }).toList
-      header_errors ::: import_errors
-    }
+    def errors: List[String] = deps.flatMap(dep => dep.header.errors)
 
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
@@ -105,13 +86,13 @@
   private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
     thy: (Document.Node.Name, Position.T)): Dependencies =
   {
-    val (name, require_pos) = thy
+    val (name, pos) = thy
 
     def message: String =
       "The error(s) above occurred for theory " + quote(name.theory) +
-        required_by(initiators) + Position.here(require_pos)
+        required_by(initiators) + Position.here(pos)
 
-    val required1 = required + thy
+    val required1 = required + name
     if (required.seen(name)) required
     else if (resources.session_base.loaded_theory(name)) required1
     else {