# HG changeset patch
# User wenzelm
# Date 1510069465 -3600
# Node ID 961285f581e6cf2141707234de74bd3b42694af2
# Parent  72d37a2e9ccad9c5559361b8e1e9e2b69dfe0000
clarifified selection: always wrt. build_graph structure;
tuned signature;

diff -r 72d37a2e9cca -r 961285f581e6 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/Admin/afp.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -37,7 +37,7 @@
 
   val sessions_structure: Sessions.T =
     Sessions.load(options, dirs = List(main_dir)).
-      selection(Sessions.Selection(sessions = sessions.toList))._2
+      selection(Sessions.Selection(sessions = sessions.toList))
 
 
   /* dependency graph */
diff -r 72d37a2e9cca -r 961285f581e6 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -32,7 +32,7 @@
       if (raw_ml_system) Nil
       else {
         val selection = Sessions.Selection(sessions = List(logic_name))
-        val (_, selected_sessions) =
+        val selected_sessions =
           sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
         selected_sessions.build_requirements(List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
diff -r 72d37a2e9cca -r 961285f581e6 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -349,7 +349,7 @@
     val global_theories = full_sessions.global_theories
 
     val selected_sessions =
-      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))._2
+      full_sessions.selection(Selection(sessions = session :: ancestor_session.toList))
     val info = selected_sessions(session)
     val ancestor = ancestor_session orElse info.parent
 
@@ -406,7 +406,7 @@
       if (focus_session) full_sessions1.imports_descendants(List(session1))
       else List(session1)
     val selected_sessions1 =
-      full_sessions1.selection(Selection(sessions = select_sessions1))._2
+      full_sessions1.selection(Selection(sessions = select_sessions1))
 
     val sessions1 = if (all_known) full_sessions1 else selected_sessions1
     val deps1 = Sessions.deps(sessions1, global_theories)
@@ -510,45 +510,6 @@
         exclude_sessions = Library.merge(exclude_sessions, other.exclude_sessions),
         session_groups = Library.merge(session_groups, other.session_groups),
         sessions = Library.merge(sessions, other.sessions))
-
-    def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
-    {
-      val bad_sessions =
-        SortedSet((base_sessions ::: exclude_sessions ::: sessions).
-          filterNot(graph.defined(_)): _*).toList
-      if (bad_sessions.nonEmpty)
-        error("Undefined session(s): " + commas_quote(bad_sessions))
-
-      val excluded =
-      {
-        val exclude_group = exclude_session_groups.toSet
-        val exclude_group_sessions =
-          (for {
-            (name, (info, _)) <- graph.iterator
-            if graph.get_node(name).groups.exists(exclude_group)
-          } yield name).toList
-        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
-      }
-
-      val pre_selected =
-      {
-        if (all_sessions) graph.keys
-        else {
-          val select_group = session_groups.toSet
-          val select = sessions.toSet ++ graph.all_succs(base_sessions)
-          (for {
-            (name, (info, _)) <- graph.iterator
-            if info.dir_selected || select(name) || graph.get_node(name).groups.exists(select_group)
-          } yield name).toList
-        }
-      }.filterNot(excluded)
-
-      val selected =
-        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
-        else pre_selected
-
-      (selected, graph.restrict(graph.all_preds(selected).toSet))
-    }
   }
 
   def make(infos: List[Info]): T =
@@ -596,9 +557,9 @@
     def build_graph_display: Graph_Display.Graph = Graph_Display.make_graph(build_graph)
     def imports_graph_display: Graph_Display.Graph = Graph_Display.make_graph(imports_graph)
 
+    def defined(name: String): Boolean = imports_graph.defined(name)
     def apply(name: String): Info = imports_graph.get_node(name)
-    def get(name: String): Option[Info] =
-      if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
+    def get(name: String): Option[Info] = if (defined(name)) Some(apply(name)) else None
 
     def global_theories: Map[String, String] =
       (Thy_Header.bootstrap_global_theories.toMap /:
@@ -615,11 +576,48 @@
               }
           })
 
-    def selection(select: Selection): (List[String], T) =
+    def selection(sel: Selection): T =
     {
-      val (_, build_graph1) = select(build_graph)
-      val (selected, imports_graph1) = select(imports_graph)
-      (selected, new T(build_graph1, imports_graph1))
+      val bad_sessions =
+        SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
+          filterNot(defined(_)): _*).toList
+      if (bad_sessions.nonEmpty)
+        error("Undefined session(s): " + commas_quote(bad_sessions))
+
+      val excluded =
+      {
+        val exclude_group = sel.exclude_session_groups.toSet
+        val exclude_group_sessions =
+          (for {
+            (name, (info, _)) <- build_graph.iterator
+            if build_graph.get_node(name).groups.exists(exclude_group)
+          } yield name).toList
+        build_graph.all_succs(exclude_group_sessions ::: sel.exclude_sessions).toSet
+      }
+
+      def restrict(graph: Graph[String, Info]): Graph[String, Info] =
+      {
+        val selected0 =
+        {
+          if (sel.all_sessions) graph.keys
+          else {
+            val select_group = sel.session_groups.toSet
+            val select = sel.sessions.toSet ++ build_graph.all_succs(sel.base_sessions)
+            (for {
+              (name, (info, _)) <- graph.iterator
+              if info.dir_selected || select(name) || apply(name).groups.exists(select_group)
+            } yield name).toList
+          }
+        }.filterNot(excluded)
+
+        val selected1 =
+          if (sel.requirements) (graph.all_preds(selected0).toSet -- selected0).toList
+          else selected0
+
+        graph.restrict(graph.all_preds(selected1).toSet)
+      }
+
+      new T(restrict(build_graph), restrict(imports_graph))
     }
 
     def build_descendants(names: List[String]): List[String] =
diff -r 72d37a2e9cca -r 961285f581e6 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -391,9 +391,9 @@
       SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
     }
 
-    val (selected, selected_sessions, deps) =
+    val (selected_sessions, deps) =
     {
-      val (selected0, selected_sessions0) =
+      val selected_sessions0 =
         full_sessions.selection(
             Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
               exclude_sessions, session_groups, sessions) ++ selection)
@@ -405,7 +405,7 @@
 
       if (soft_build && !fresh_build) {
         val outdated =
-          selected0.flatMap(name =>
+          selected_sessions0.build_topological_order.flatMap(name =>
             store.find_database(name) match {
               case Some(database) =>
                 using(SQLite.open_database(database))(store.read_build(_, name)) match {
@@ -415,14 +415,14 @@
                 }
               case None => Some(name)
             })
-        val (selected, selected_sessions) =
+        val selected_sessions =
           full_sessions.selection(Sessions.Selection(sessions = outdated))
         val deps =
           Sessions.deps(selected_sessions, full_sessions.global_theories, inlined_files = true)
             .check_errors
-        (selected, selected_sessions, deps)
+        (selected_sessions, deps)
       }
-      else (selected0, selected_sessions0, deps0)
+      else (selected_sessions0, deps0)
     }
 
 
@@ -450,7 +450,7 @@
 
     // optional cleanup
     if (clean_build) {
-      for (name <- full_sessions.build_descendants(selected)) {
+      for (name <- full_sessions.build_descendants(selected_sessions.build_topological_order)) {
         val files =
           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
             map(store.output_dir + _).filter(_.is_file)
diff -r 72d37a2e9cca -r 961285f581e6 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Tue Nov 07 15:50:36 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Tue Nov 07 16:44:25 2017 +0100
@@ -100,7 +100,7 @@
     verbose: Boolean = false) =
   {
     val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
-    val (selected, selected_sessions) = full_sessions.selection(selection)
+    val selected_sessions = full_sessions.selection(selection)
 
     val deps =
       Sessions.deps(selected_sessions, full_sessions.global_theories,
@@ -109,41 +109,42 @@
     val root_keywords = Sessions.root_syntax.keywords
 
     if (operation_imports) {
-      val report_imports: List[Report] = selected.map((session_name: String) =>
-      {
-        val info = selected_sessions(session_name)
-        val session_base = deps(session_name)
+      val report_imports: List[Report] =
+        selected_sessions.build_topological_order.map((session_name: String) =>
+          {
+            val info = selected_sessions(session_name)
+            val session_base = deps(session_name)
 
-        val declared_imports =
-          selected_sessions.imports_requirements(List(session_name)).toSet
+            val declared_imports =
+              selected_sessions.imports_requirements(List(session_name)).toSet
 
-        val extra_imports =
-          (for {
-            (_, a) <- session_base.known.theories.iterator
-            if session_base.theory_qualifier(a) == info.name
-            b <- deps.all_known.get_file(a.path.file)
-            qualifier = session_base.theory_qualifier(b)
-            if !declared_imports.contains(qualifier)
-          } yield qualifier).toSet
+            val extra_imports =
+              (for {
+                (_, a) <- session_base.known.theories.iterator
+                if session_base.theory_qualifier(a) == info.name
+                b <- deps.all_known.get_file(a.path.file)
+                qualifier = session_base.theory_qualifier(b)
+                if !declared_imports.contains(qualifier)
+              } yield qualifier).toSet
 
-        val loaded_imports =
-          selected_sessions.imports_requirements(
-            session_base.loaded_theories.keys.map(a =>
-              session_base.theory_qualifier(session_base.known.theories(a))))
-          .toSet - session_name
+            val loaded_imports =
+              selected_sessions.imports_requirements(
+                session_base.loaded_theories.keys.map(a =>
+                  session_base.theory_qualifier(session_base.known.theories(a))))
+              .toSet - session_name
 
-        val minimal_imports =
-          loaded_imports.filter(s1 =>
-            !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
+            val minimal_imports =
+              loaded_imports.filter(s1 =>
+                !loaded_imports.exists(s2 => selected_sessions.imports_graph.is_edge(s1, s2)))
 
-        def make_result(set: Set[String]): Option[List[String]] =
-          if (set.isEmpty) None
-          else Some(selected_sessions.imports_topological_order.filter(set))
+            def make_result(set: Set[String]): Option[List[String]] =
+              if (set.isEmpty) None
+              else Some(selected_sessions.imports_topological_order.filter(set))
 
-        Report(info, declared_imports, make_result(extra_imports),
-          if (loaded_imports == declared_imports - session_name) None
-          else make_result(minimal_imports))
-      })
+            Report(info, declared_imports, make_result(extra_imports),
+              if (loaded_imports == declared_imports - session_name) None
+              else make_result(minimal_imports))
+          })
 
       progress.echo("\nPotential session imports:")
       for {
@@ -172,34 +173,34 @@
     if (operation_update) {
       progress.echo("\nUpdate theory imports" + update_message + ":")
       val updates =
-        selected.flatMap(session_name =>
-        {
-          val info = selected_sessions(session_name)
-          val session_base = deps(session_name)
-          val session_resources = new Resources(session_base)
-          val imports_base = session_base.get_imports
-          val imports_resources = new Resources(imports_base)
+        selected_sessions.build_topological_order.flatMap(session_name =>
+          {
+            val info = selected_sessions(session_name)
+            val session_base = deps(session_name)
+            val session_resources = new Resources(session_base)
+            val imports_base = session_base.get_imports
+            val imports_resources = new Resources(imports_base)
 
-          def standard_import(qualifier: String, dir: String, s: String): String =
-            imports_resources.standard_import(session_base, qualifier, dir, s)
+            def standard_import(qualifier: String, dir: String, s: String): String =
+              imports_resources.standard_import(session_base, qualifier, dir, s)
 
-          val updates_root =
-            for {
-              (_, pos) <- info.theories.flatMap(_._2)
-              upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
-            } yield upd
+            val updates_root =
+              for {
+                (_, pos) <- info.theories.flatMap(_._2)
+                upd <- update_name(root_keywords, pos, standard_import(info.name, info.dir.implode, _))
+              } yield upd
 
-          val updates_theories =
-            for {
-              (_, name) <- session_base.known.theories_local.toList
-              if session_base.theory_qualifier(name) == info.name
-              (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
-              upd <- update_name(session_base.overall_syntax.keywords, pos,
-                standard_import(session_base.theory_qualifier(name), name.master_dir, _))
-            } yield upd
+            val updates_theories =
+              for {
+                (_, name) <- session_base.known.theories_local.toList
+                if session_base.theory_qualifier(name) == info.name
+                (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
+                upd <- update_name(session_base.overall_syntax.keywords, pos,
+                  standard_import(session_base.theory_qualifier(name), name.master_dir, _))
+              } yield upd
 
-          updates_root ::: updates_theories
-        })
+            updates_root ::: updates_theories
+          })
 
       val file_updates = (Multi_Map.empty[JFile, Update] /: updates)(_ + _)
       val conflicts =
@@ -311,15 +312,14 @@
           verbose = verbose)
       }
       else if (operation_update && incremental_update) {
-        val (selected, selected_sessions) =
-          Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
-        selected_sessions.imports_topological_order.foreach(name =>
-        {
-          imports(options, operation_update = operation_update, progress = progress,
-            update_message = " for session " + quote(name),
-            selection = Sessions.Selection(sessions = List(name)),
-            dirs = dirs ::: select_dirs, verbose = verbose)
-        })
+        Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection).
+          imports_topological_order.foreach(name =>
+            {
+              imports(options, operation_update = operation_update, progress = progress,
+                update_message = " for session " + quote(name),
+                selection = Sessions.Selection(sessions = List(name)),
+                dirs = dirs ::: select_dirs, verbose = verbose)
+            })
       }
     })
 }