--- a/src/Pure/PIDE/command.scala Mon Sep 16 16:00:10 2019 +0200
+++ b/src/Pure/PIDE/command.scala Mon Sep 16 19:35:08 2019 +0200
@@ -524,20 +524,7 @@
for { ((import_name, pos), s) <- imports_pos zip raw_imports if !can_import(import_name) }
yield {
val completion =
- if (Thy_Header.is_base_name(s)) {
- val completed = Completion.completed(import_name.theory_base_name)
- val qualifier = resources.session_base.theory_qualifier(node_name)
- val dir = node_name.master_dir
- for {
- known_name <- resources.session_base.known.theory_names
- if completed(known_name.theory_base_name)
- }
- yield {
- resources.standard_import(
- resources.session_base, qualifier, dir, known_name.theory)
- }
- }.sorted
- else Nil
+ if (Thy_Header.is_base_name(s)) resources.complete_import_name(node_name, s) else Nil
val msg =
"Bad theory import " +
Markup.Path(import_name.node).markup(quote(import_name.toString)) +