equal
deleted
inserted
replaced
78 } yield name).toSet |
78 } yield name).toSet |
79 |
79 |
80 def standard_import(qualifier: String, dir: String, s: String): String = |
80 def standard_import(qualifier: String, dir: String, s: String): String = |
81 { |
81 { |
82 val name = imports_resources.import_name(qualifier, dir, s) |
82 val name = imports_resources.import_name(qualifier, dir, s) |
|
83 val file = Path.explode(name.node).file |
83 val s1 = |
84 val s1 = |
84 if (!local_theories.contains(name)) s |
85 imports_resources.session_base.known.get_file(file) match { |
85 else if (session_resources.theory_qualifier(name) != qualifier) name.theory |
86 case Some(name1) if session_resources.theory_qualifier(name1) != qualifier => |
86 else if (Thy_Header.is_base_name(s)) name.theory_base_name |
87 name1.theory |
87 else s |
88 case Some(name1) if Thy_Header.is_base_name(s) => |
88 val name1 = imports_resources.import_name(qualifier, dir, s1) |
89 name1.theory_base_name |
89 if (name == name1) s1 else s |
90 case _ => s |
|
91 } |
|
92 val name2 = imports_resources.import_name(qualifier, dir, s1) |
|
93 if (name.node == name2.node) s1 else s |
90 } |
94 } |
91 |
95 |
92 val updates_root = |
96 val updates_root = |
93 for { |
97 for { |
94 (_, pos) <- info.theories.flatMap(_._2) |
98 (_, pos) <- info.theories.flatMap(_._2) |