src/Pure/Tools/imports.scala
changeset 67025 961285f581e6
parent 67023 e27e05d6f2a7
child 67026 687c822ee5e3
     1.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 15:50:36 2017 +0100
     1.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 16:44:25 2017 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4      verbose: Boolean = false) =
     1.5    {
     1.6      val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
     1.7 -    val (selected, selected_sessions) = full_sessions.selection(selection)
     1.8 +    val selected_sessions = full_sessions.selection(selection)
     1.9  
    1.10      val deps =
    1.11        Sessions.deps(selected_sessions, full_sessions.global_theories,
    1.12 @@ -109,41 +109,42 @@
    1.13      val root_keywords = Sessions.root_syntax.keywords
    1.14  
    1.15      if (operation_imports) {
    1.16 -      val report_imports: List[Report] = selected.map((session_name: String) =>
    1.17 -      {
    1.18 -        val info = selected_sessions(session_name)
    1.19 -        val session_base = deps(session_name)
    1.20 +      val report_imports: List[Report] =
    1.21 +        selected_sessions.build_topological_order.map((session_name: String) =>
    1.22 +          {
    1.23 +            val info = selected_sessions(session_name)
    1.24 +            val session_base = deps(session_name)
    1.25  
    1.26 -        val declared_imports =
    1.27 -          selected_sessions.imports_requirements(List(session_name)).toSet
    1.28 +            val declared_imports =
    1.29 +              selected_sessions.imports_requirements(List(session_name)).toSet
    1.30  
    1.31 -        val extra_imports =
    1.32 -          (for {
    1.33 -            (_, a) <- session_base.known.theories.iterator
    1.34 -            if session_base.theory_qualifier(a) == info.name
    1.35 -            b <- deps.all_known.get_file(a.path.file)
    1.36 -            qualifier = session_base.theory_qualifier(b)
    1.37 -            if !declared_imports.contains(qualifier)
    1.38 -          } yield qualifier).toSet
    1.39 +            val extra_imports =
    1.40 +              (for {
    1.41 +                (_, a) <- session_base.known.theories.iterator
    1.42 +                if session_base.theory_qualifier(a) == info.name
    1.43 +                b <- deps.all_known.get_file(a.path.file)
    1.44 +                qualifier = session_base.theory_qualifier(b)
    1.45 +                if !declared_imports.contains(qualifier)
    1.46 +              } yield qualifier).toSet
    1.47  
    1.48 -        val loaded_imports =
    1.49 -          selected_sessions.imports_requirements(
    1.50 -            session_base.loaded_theories.keys.map(a =>
    1.51 -              session_base.theory_qualifier(session_base.known.theories(a))))
    1.52 -          .toSet - session_name
    1.53 +            val loaded_imports =
    1.54 +              selected_sessions.imports_requirements(
    1.55 +                session_base.loaded_theories.keys.map(a =>
    1.56 +                  session_base.theory_qualifier(session_base.known.theories(a))))
    1.57 +              .toSet - session_name
    1.58  
    1.59 -        val minimal_imports =
    1.60 -          loaded_imports.filter(s1 =>
    1.61 -            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    1.62 +            val minimal_imports =
    1.63 +              loaded_imports.filter(s1 =>
    1.64 +                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    1.65  
    1.66 -        def make_result(set: Set[String]): Option[List[String]] =
    1.67 -          if (set.isEmpty) None
    1.68 -          else Some(selected_sessions.imports_topological_order.filter(set))
    1.69 +            def make_result(set: Set[String]): Option[List[String]] =
    1.70 +              if (set.isEmpty) None
    1.71 +              else Some(selected_sessions.imports_topological_order.filter(set))
    1.72  
    1.73 -        Report(info, declared_imports, make_result(extra_imports),
    1.74 -          if (loaded_imports == declared_imports - session_name) None
    1.75 -          else make_result(minimal_imports))
    1.76 -      })
    1.77 +            Report(info, declared_imports, make_result(extra_imports),
    1.78 +              if (loaded_imports == declared_imports - session_name) None
    1.79 +              else make_result(minimal_imports))
    1.80 +          })
    1.81  
    1.82        progress.echo("\nPotential session imports:")
    1.83        for {
    1.84 @@ -172,34 +173,34 @@
    1.85      if (operation_update) {
    1.86        progress.echo("\nUpdate theory imports" + update_message + ":")
    1.87        val updates =
    1.88 -        selected.flatMap(session_name =>
    1.89 -        {
    1.90 -          val info = selected_sessions(session_name)
    1.91 -          val session_base = deps(session_name)
    1.92 -          val session_resources = new Resources(session_base)
    1.93 -          val imports_base = session_base.get_imports
    1.94 -          val imports_resources = new Resources(imports_base)
    1.95 +        selected_sessions.build_topological_order.flatMap(session_name =>
    1.96 +          {
    1.97 +            val info = selected_sessions(session_name)
    1.98 +            val session_base = deps(session_name)
    1.99 +            val session_resources = new Resources(session_base)
   1.100 +            val imports_base = session_base.get_imports
   1.101 +            val imports_resources = new Resources(imports_base)
   1.102  
   1.103 -          def standard_import(qualifier: String, dir: String, s: String): String =
   1.104 -            imports_resources.standard_import(session_base, qualifier, dir, s)
   1.105 +            def standard_import(qualifier: String, dir: String, s: String): String =
   1.106 +              imports_resources.standard_import(session_base, qualifier, dir, s)
   1.107  
   1.108 -          val updates_root =
   1.109 -            for {
   1.110 -              (_, pos) <- info.theories.flatMap(_._2)
   1.111 -              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   1.112 -            } yield upd
   1.113 +            val updates_root =
   1.114 +              for {
   1.115 +                (_, pos) <- info.theories.flatMap(_._2)
   1.116 +                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   1.117 +              } yield upd
   1.118  
   1.119 -          val updates_theories =
   1.120 -            for {
   1.121 -              (_, name) <- session_base.known.theories_local.toList
   1.122 -              if session_base.theory_qualifier(name) == info.name
   1.123 -              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   1.124 -              upd <- update_name(session_base.overall_syntax.keywords, pos,
   1.125 -                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   1.126 -            } yield upd
   1.127 +            val updates_theories =
   1.128 +              for {
   1.129 +                (_, name) <- session_base.known.theories_local.toList
   1.130 +                if session_base.theory_qualifier(name) == info.name
   1.131 +                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   1.132 +                upd <- update_name(session_base.overall_syntax.keywords, pos,
   1.133 +                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   1.134 +              } yield upd
   1.135  
   1.136 -          updates_root ::: updates_theories
   1.137 -        })
   1.138 +            updates_root ::: updates_theories
   1.139 +          })
   1.140  
   1.141        val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   1.142        val conflicts =
   1.143 @@ -311,15 +312,14 @@
   1.144            verbose = verbose)
   1.145        }
   1.146        else if (operation_update && incremental_update) {
   1.147 -        val (selected, selected_sessions) =
   1.148 -          Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
   1.149 -        selected_sessions.imports_topological_order.foreach(name =>
   1.150 -        {
   1.151 -          imports(options, operation_update = operation_update, progress = progress,
   1.152 -            update_message = " for session " + quote(name),
   1.153 -            selection = Sessions.Selection(sessions = List(name)),
   1.154 -            dirs = dirs ::: select_dirs, verbose = verbose)
   1.155 -        })
   1.156 +        Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection).
   1.157 +          imports_topological_order.foreach(name =>
   1.158 +            {
   1.159 +              imports(options, operation_update = operation_update, progress = progress,
   1.160 +                update_message = " for session " + quote(name),
   1.161 +                selection = Sessions.Selection(sessions = List(name)),
   1.162 +                dirs = dirs ::: select_dirs, verbose = verbose)
   1.163 +            })
   1.164        }
   1.165      })
   1.166  }