src/Pure/Tools/imports.scala
changeset 68204 a554da2811f2
parent 67026 687c822ee5e3
child 68304 09270aa40884
     1.1 --- a/src/Pure/Tools/imports.scala	Thu May 17 14:50:48 2018 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Thu May 17 15:38:36 2018 +0200
     1.3 @@ -100,23 +100,22 @@
     1.4      verbose: Boolean = false) =
     1.5    {
     1.6      val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
     1.7 -    val selected_sessions = full_sessions.selection(selection)
     1.8  
     1.9      val deps =
    1.10 -      Sessions.deps(selected_sessions, full_sessions.global_theories,
    1.11 +      Sessions.deps(full_sessions.selection(selection), full_sessions.global_theories,
    1.12          progress = progress, verbose = verbose).check_errors
    1.13  
    1.14      val root_keywords = Sessions.root_syntax.keywords
    1.15  
    1.16      if (operation_imports) {
    1.17        val report_imports: List[Report] =
    1.18 -        selected_sessions.build_topological_order.map((session_name: String) =>
    1.19 +        deps.sessions_structure.build_topological_order.map((session_name: String) =>
    1.20            {
    1.21 -            val info = selected_sessions(session_name)
    1.22 +            val info = deps.sessions_structure(session_name)
    1.23              val session_base = deps(session_name)
    1.24  
    1.25              val declared_imports =
    1.26 -              selected_sessions.imports_requirements(List(session_name)).toSet
    1.27 +              deps.sessions_structure.imports_requirements(List(session_name)).toSet
    1.28  
    1.29              val extra_imports =
    1.30                (for {
    1.31 @@ -128,18 +127,18 @@
    1.32                } yield qualifier).toSet
    1.33  
    1.34              val loaded_imports =
    1.35 -              selected_sessions.imports_requirements(
    1.36 +              deps.sessions_structure.imports_requirements(
    1.37                  session_base.loaded_theories.keys.map(a =>
    1.38                    session_base.theory_qualifier(session_base.known.theories(a))))
    1.39                .toSet - session_name
    1.40  
    1.41              val minimal_imports =
    1.42                loaded_imports.filter(s1 =>
    1.43 -                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    1.44 +                !loaded_imports.exists(s2 => deps.sessions_structure.imports_graph.is_edge(s1, s2)))
    1.45  
    1.46              def make_result(set: Set[String]): Option[List[String]] =
    1.47                if (set.isEmpty) None
    1.48 -              else Some(selected_sessions.imports_topological_order.filter(set))
    1.49 +              else Some(deps.sessions_structure.imports_topological_order.filter(set))
    1.50  
    1.51              Report(info, declared_imports, make_result(extra_imports),
    1.52                if (loaded_imports == declared_imports - session_name) None
    1.53 @@ -173,9 +172,9 @@
    1.54      if (operation_update) {
    1.55        progress.echo("\nUpdate theory imports" + update_message + ":")
    1.56        val updates =
    1.57 -        selected_sessions.build_topological_order.flatMap(session_name =>
    1.58 +        deps.sessions_structure.build_topological_order.flatMap(session_name =>
    1.59            {
    1.60 -            val info = selected_sessions(session_name)
    1.61 +            val info = deps.sessions_structure(session_name)
    1.62              val session_base = deps(session_name)
    1.63              val session_resources = new Resources(session_base)
    1.64              val imports_base = session_base.get_imports