diff -r 0f2ff88f823e -r d0909b5d88eb src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Tue Jul 21 12:37:00 2020 +0200 +++ b/src/Pure/Thy/sessions.scala Tue Jul 21 19:40:38 2020 +0200 @@ -249,22 +249,15 @@ val known_loaded_files = imports_base.known_loaded_files ++ loaded_files - val used_theories = - for ((options, name) <- dependencies.adjunct_theories) - yield (name, options) - - def used_theories_session_iterator: Iterator[Document.Node.Name] = - for { - (name, _) <- used_theories.iterator - if imports_base.theory_qualifier(name) == session_name - } yield name + val used_theories_session = + dependencies.theories.filter(name => imports_base.theory_qualifier(name) == session_name) val dir_errors = { val ok = info.dirs.map(_.canonical_file).toSet val bad = (for { - name <- used_theories_session_iterator + name <- used_theories_session.iterator path = name.master_dir_path if !ok(path.canonical_file) path1 = File.relative_path(info.dir.canonical, path).getOrElse(path) @@ -280,7 +273,7 @@ val errs3 = for (p <- info.dirs if !p.is_dir) yield "No such directory: " + p val errs4 = (for { - name <- used_theories_session_iterator + name <- used_theories_session.iterator name1 <- resources.find_theory_node(name.theory) if name.node != name1.node } yield "Incoherent theory file import:\n " + name.path + " vs. \n " + name1.path) @@ -307,7 +300,7 @@ session_directories = sessions_structure.session_directories, global_theories = sessions_structure.global_theories, loaded_theories = dependencies.loaded_theories, - used_theories = used_theories, + used_theories = dependencies.theories_adjunct, known_theories = known_theories, known_loaded_files = known_loaded_files, overall_syntax = overall_syntax,