clarifified selection: always wrt. build_graph structure;
authorwenzelm
Tue Nov 07 16:44:25 2017 +0100 (17 months ago)
changeset 67025961285f581e6
parent 67024 72d37a2e9cca
child 67026 687c822ee5e3
clarifified selection: always wrt. build_graph structure;
tuned signature;
src/Pure/Admin/afp.scala
src/Pure/ML/ml_process.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Admin/afp.scala	Tue Nov 07 15:50:36 2017 +0100
     1.2 +++ b/src/Pure/Admin/afp.scala	Tue Nov 07 16:44:25 2017 +0100
     1.3 @@ -37,7 +37,7 @@
     1.4  
     1.5    val sessions_structure: Sessions.T =
     1.6      Sessions.load(options, dirs = List(main_dir)).
     1.7 -      selection(Sessions.Selection(sessions = sessions.toList))._2
     1.8 +      selection(Sessions.Selection(sessions = sessions.toList))
     1.9  
    1.10  
    1.11    /* dependency graph */
     2.1 --- a/src/Pure/ML/ml_process.scala	Tue Nov 07 15:50:36 2017 +0100
     2.2 +++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
     2.3 @@ -32,7 +32,7 @@
     2.4        if (raw_ml_system) Nil
     2.5        else {
     2.6          val selection = Sessions.Selection(sessions = List(logic_name))
     2.7 -        val (_, selected_sessions) =
     2.8 +        val selected_sessions =
     2.9            sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
    2.10          selected_sessions.build_requirements(List(logic_name)).
    2.11            map(a => File.platform_path(store.heap(a)))
     3.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 15:50:36 2017 +0100
     3.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 16:44:25 2017 +0100
     3.3 @@ -349,7 +349,7 @@
     3.4      val global_theories = full_sessions.global_theories
     3.5  
     3.6      val selected_sessions =
     3.7 -      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
     3.8 +      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
     3.9      val info = selected_sessions(session)
    3.10      val ancestor = ancestor_session orElse info.parent
    3.11  
    3.12 @@ -406,7 +406,7 @@
    3.13        if (focus_session) full_sessions1.imports_descendants(List(session1))
    3.14        else List(session1)
    3.15      val selected_sessions1 =
    3.16 -      full_sessions1.selection(Selection(sessions = select_sessions1))._2
    3.17 +      full_sessions1.selection(Selection(sessions = select_sessions1))
    3.18  
    3.19      val sessions1 = if (all_known) full_sessions1 else selected_sessions1
    3.20      val deps1 = Sessions.deps(sessions1, global_theories)
    3.21 @@ -510,45 +510,6 @@
    3.22          exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
    3.23          session_groups = Library.merge(session_groups, other.session_groups),
    3.24          sessions = Library.merge(sessions, other.sessions))
    3.25 -
    3.26 -    def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    3.27 -    {
    3.28 -      val bad_sessions =
    3.29 -        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
    3.30 -          filterNot(graph.defined(_)): _*).toList
    3.31 -      if (bad_sessions.nonEmpty)
    3.32 -        error("Undefined session(s): " + commas_quote(bad_sessions))
    3.33 -
    3.34 -      val excluded =
    3.35 -      {
    3.36 -        val exclude_group = exclude_session_groups.toSet
    3.37 -        val exclude_group_sessions =
    3.38 -          (for {
    3.39 -            (name, (info, _)) <- graph.iterator
    3.40 -            if graph.get_node(name).groups.exists(exclude_group)
    3.41 -          } yield name).toList
    3.42 -        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
    3.43 -      }
    3.44 -
    3.45 -      val pre_selected =
    3.46 -      {
    3.47 -        if (all_sessions) graph.keys
    3.48 -        else {
    3.49 -          val select_group = session_groups.toSet
    3.50 -          val select = sessions.toSet ++ graph.all_succs(base_sessions)
    3.51 -          (for {
    3.52 -            (name, (info, _)) <- graph.iterator
    3.53 -            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
    3.54 -          } yield name).toList
    3.55 -        }
    3.56 -      }.filterNot(excluded)
    3.57 -
    3.58 -      val selected =
    3.59 -        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
    3.60 -        else pre_selected
    3.61 -
    3.62 -      (selected, graph.restrict(graph.all_preds(selected).toSet))
    3.63 -    }
    3.64    }
    3.65  
    3.66    def make(infos: List[Info]): T =
    3.67 @@ -596,9 +557,9 @@
    3.68      def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
    3.69      def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
    3.70  
    3.71 +    def defined(name: String): Boolean = imports_graph.defined(name)
    3.72      def apply(name: String): Info = imports_graph.get_node(name)
    3.73 -    def get(name: String): Option[Info] =
    3.74 -      if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
    3.75 +    def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
    3.76  
    3.77      def global_theories: Map[String, String] =
    3.78        (Thy_Header.bootstrap_global_theories.toMap /:
    3.79 @@ -615,11 +576,48 @@
    3.80                }
    3.81            })
    3.82  
    3.83 -    def selection(select: Selection): (List[String], T) =
    3.84 +    def selection(sel: Selection): T =
    3.85      {
    3.86 -      val (_, build_graph1) = select(build_graph)
    3.87 -      val (selected, imports_graph1) = select(imports_graph)
    3.88 -      (selected, new T(build_graph1, imports_graph1))
    3.89 +      val bad_sessions =
    3.90 +        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
    3.91 +          filterNot(defined(_)): _*).toList
    3.92 +      if (bad_sessions.nonEmpty)
    3.93 +        error("Undefined session(s): " + commas_quote(bad_sessions))
    3.94 +
    3.95 +      val excluded =
    3.96 +      {
    3.97 +        val exclude_group = sel.exclude_session_groups.toSet
    3.98 +        val exclude_group_sessions =
    3.99 +          (for {
   3.100 +            (name, (info, _)) <- build_graph.iterator
   3.101 +            if build_graph.get_node(name).groups.exists(exclude_group)
   3.102 +          } yield name).toList
   3.103 +        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
   3.104 +      }
   3.105 +
   3.106 +      def restrict(graph: Graph[String, Info]): Graph[String, Info] =
   3.107 +      {
   3.108 +        val selected0 =
   3.109 +        {
   3.110 +          if (sel.all_sessions) graph.keys
   3.111 +          else {
   3.112 +            val select_group = sel.session_groups.toSet
   3.113 +            val select = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
   3.114 +            (for {
   3.115 +              (name, (info, _)) <- graph.iterator
   3.116 +              if info.dir_selected || select(name) || apply(name).groups.exists(select_group)
   3.117 +            } yield name).toList
   3.118 +          }
   3.119 +        }.filterNot(excluded)
   3.120 +
   3.121 +        val selected1 =
   3.122 +          if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
   3.123 +          else selected0
   3.124 +
   3.125 +        graph.restrict(graph.all_preds(selected1).toSet)
   3.126 +      }
   3.127 +
   3.128 +      new T(restrict(build_graph), restrict(imports_graph))
   3.129      }
   3.130  
   3.131      def build_descendants(names: List[String]): List[String] =
     4.1 --- a/src/Pure/Tools/build.scala	Tue Nov 07 15:50:36 2017 +0100
     4.2 +++ b/src/Pure/Tools/build.scala	Tue Nov 07 16:44:25 2017 +0100
     4.3 @@ -391,9 +391,9 @@
     4.4        SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     4.5      }
     4.6  
     4.7 -    val (selected, selected_sessions, deps) =
     4.8 +    val (selected_sessions, deps) =
     4.9      {
    4.10 -      val (selected0, selected_sessions0) =
    4.11 +      val selected_sessions0 =
    4.12          full_sessions.selection(
    4.13              Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    4.14                exclude_sessions, session_groups, sessions) ++ selection)
    4.15 @@ -405,7 +405,7 @@
    4.16  
    4.17        if (soft_build && !fresh_build) {
    4.18          val outdated =
    4.19 -          selected0.flatMap(name =>
    4.20 +          selected_sessions0.build_topological_order.flatMap(name =>
    4.21              store.find_database(name) match {
    4.22                case Some(database) =>
    4.23                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    4.24 @@ -415,14 +415,14 @@
    4.25                  }
    4.26                case None => Some(name)
    4.27              })
    4.28 -        val (selected, selected_sessions) =
    4.29 +        val selected_sessions =
    4.30            full_sessions.selection(Sessions.Selection(sessions = outdated))
    4.31          val deps =
    4.32            Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
    4.33              .check_errors
    4.34 -        (selected, selected_sessions, deps)
    4.35 +        (selected_sessions, deps)
    4.36        }
    4.37 -      else (selected0, selected_sessions0, deps0)
    4.38 +      else (selected_sessions0, deps0)
    4.39      }
    4.40  
    4.41  
    4.42 @@ -450,7 +450,7 @@
    4.43  
    4.44      // optional cleanup
    4.45      if (clean_build) {
    4.46 -      for (name <- full_sessions.build_descendants(selected)) {
    4.47 +      for (name <- full_sessions.build_descendants(selected_sessions.build_topological_order)) {
    4.48          val files =
    4.49            List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
    4.50              map(store.output_dir + _).filter(_.is_file)
     5.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 15:50:36 2017 +0100
     5.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 16:44:25 2017 +0100
     5.3 @@ -100,7 +100,7 @@
     5.4      verbose: Boolean = false) =
     5.5    {
     5.6      val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
     5.7 -    val (selected, selected_sessions) = full_sessions.selection(selection)
     5.8 +    val selected_sessions = full_sessions.selection(selection)
     5.9  
    5.10      val deps =
    5.11        Sessions.deps(selected_sessions, full_sessions.global_theories,
    5.12 @@ -109,41 +109,42 @@
    5.13      val root_keywords = Sessions.root_syntax.keywords
    5.14  
    5.15      if (operation_imports) {
    5.16 -      val report_imports: List[Report] = selected.map((session_name: String) =>
    5.17 -      {
    5.18 -        val info = selected_sessions(session_name)
    5.19 -        val session_base = deps(session_name)
    5.20 +      val report_imports: List[Report] =
    5.21 +        selected_sessions.build_topological_order.map((session_name: String) =>
    5.22 +          {
    5.23 +            val info = selected_sessions(session_name)
    5.24 +            val session_base = deps(session_name)
    5.25  
    5.26 -        val declared_imports =
    5.27 -          selected_sessions.imports_requirements(List(session_name)).toSet
    5.28 +            val declared_imports =
    5.29 +              selected_sessions.imports_requirements(List(session_name)).toSet
    5.30  
    5.31 -        val extra_imports =
    5.32 -          (for {
    5.33 -            (_, a) <- session_base.known.theories.iterator
    5.34 -            if session_base.theory_qualifier(a) == info.name
    5.35 -            b <- deps.all_known.get_file(a.path.file)
    5.36 -            qualifier = session_base.theory_qualifier(b)
    5.37 -            if !declared_imports.contains(qualifier)
    5.38 -          } yield qualifier).toSet
    5.39 +            val extra_imports =
    5.40 +              (for {
    5.41 +                (_, a) <- session_base.known.theories.iterator
    5.42 +                if session_base.theory_qualifier(a) == info.name
    5.43 +                b <- deps.all_known.get_file(a.path.file)
    5.44 +                qualifier = session_base.theory_qualifier(b)
    5.45 +                if !declared_imports.contains(qualifier)
    5.46 +              } yield qualifier).toSet
    5.47  
    5.48 -        val loaded_imports =
    5.49 -          selected_sessions.imports_requirements(
    5.50 -            session_base.loaded_theories.keys.map(a =>
    5.51 -              session_base.theory_qualifier(session_base.known.theories(a))))
    5.52 -          .toSet - session_name
    5.53 +            val loaded_imports =
    5.54 +              selected_sessions.imports_requirements(
    5.55 +                session_base.loaded_theories.keys.map(a =>
    5.56 +                  session_base.theory_qualifier(session_base.known.theories(a))))
    5.57 +              .toSet - session_name
    5.58  
    5.59 -        val minimal_imports =
    5.60 -          loaded_imports.filter(s1 =>
    5.61 -            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    5.62 +            val minimal_imports =
    5.63 +              loaded_imports.filter(s1 =>
    5.64 +                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
    5.65  
    5.66 -        def make_result(set: Set[String]): Option[List[String]] =
    5.67 -          if (set.isEmpty) None
    5.68 -          else Some(selected_sessions.imports_topological_order.filter(set))
    5.69 +            def make_result(set: Set[String]): Option[List[String]] =
    5.70 +              if (set.isEmpty) None
    5.71 +              else Some(selected_sessions.imports_topological_order.filter(set))
    5.72  
    5.73 -        Report(info, declared_imports, make_result(extra_imports),
    5.74 -          if (loaded_imports == declared_imports - session_name) None
    5.75 -          else make_result(minimal_imports))
    5.76 -      })
    5.77 +            Report(info, declared_imports, make_result(extra_imports),
    5.78 +              if (loaded_imports == declared_imports - session_name) None
    5.79 +              else make_result(minimal_imports))
    5.80 +          })
    5.81  
    5.82        progress.echo("\nPotential session imports:")
    5.83        for {
    5.84 @@ -172,34 +173,34 @@
    5.85      if (operation_update) {
    5.86        progress.echo("\nUpdate theory imports" + update_message + ":")
    5.87        val updates =
    5.88 -        selected.flatMap(session_name =>
    5.89 -        {
    5.90 -          val info = selected_sessions(session_name)
    5.91 -          val session_base = deps(session_name)
    5.92 -          val session_resources = new Resources(session_base)
    5.93 -          val imports_base = session_base.get_imports
    5.94 -          val imports_resources = new Resources(imports_base)
    5.95 +        selected_sessions.build_topological_order.flatMap(session_name =>
    5.96 +          {
    5.97 +            val info = selected_sessions(session_name)
    5.98 +            val session_base = deps(session_name)
    5.99 +            val session_resources = new Resources(session_base)
   5.100 +            val imports_base = session_base.get_imports
   5.101 +            val imports_resources = new Resources(imports_base)
   5.102  
   5.103 -          def standard_import(qualifier: String, dir: String, s: String): String =
   5.104 -            imports_resources.standard_import(session_base, qualifier, dir, s)
   5.105 +            def standard_import(qualifier: String, dir: String, s: String): String =
   5.106 +              imports_resources.standard_import(session_base, qualifier, dir, s)
   5.107  
   5.108 -          val updates_root =
   5.109 -            for {
   5.110 -              (_, pos) <- info.theories.flatMap(_._2)
   5.111 -              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   5.112 -            } yield upd
   5.113 +            val updates_root =
   5.114 +              for {
   5.115 +                (_, pos) <- info.theories.flatMap(_._2)
   5.116 +                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
   5.117 +              } yield upd
   5.118  
   5.119 -          val updates_theories =
   5.120 -            for {
   5.121 -              (_, name) <- session_base.known.theories_local.toList
   5.122 -              if session_base.theory_qualifier(name) == info.name
   5.123 -              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   5.124 -              upd <- update_name(session_base.overall_syntax.keywords, pos,
   5.125 -                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   5.126 -            } yield upd
   5.127 +            val updates_theories =
   5.128 +              for {
   5.129 +                (_, name) <- session_base.known.theories_local.toList
   5.130 +                if session_base.theory_qualifier(name) == info.name
   5.131 +                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
   5.132 +                upd <- update_name(session_base.overall_syntax.keywords, pos,
   5.133 +                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
   5.134 +              } yield upd
   5.135  
   5.136 -          updates_root ::: updates_theories
   5.137 -        })
   5.138 +            updates_root ::: updates_theories
   5.139 +          })
   5.140  
   5.141        val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
   5.142        val conflicts =
   5.143 @@ -311,15 +312,14 @@
   5.144            verbose = verbose)
   5.145        }
   5.146        else if (operation_update && incremental_update) {
   5.147 -        val (selected, selected_sessions) =
   5.148 -          Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
   5.149 -        selected_sessions.imports_topological_order.foreach(name =>
   5.150 -        {
   5.151 -          imports(options, operation_update = operation_update, progress = progress,
   5.152 -            update_message = " for session " + quote(name),
   5.153 -            selection = Sessions.Selection(sessions = List(name)),
   5.154 -            dirs = dirs ::: select_dirs, verbose = verbose)
   5.155 -        })
   5.156 +        Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection).
   5.157 +          imports_topological_order.foreach(name =>
   5.158 +            {
   5.159 +              imports(options, operation_update = operation_update, progress = progress,
   5.160 +                update_message = " for session " + quote(name),
   5.161 +                selection = Sessions.Selection(sessions = List(name)),
   5.162 +                dirs = dirs ::: select_dirs, verbose = verbose)
   5.163 +            })
   5.164        }
   5.165      })
   5.166  }