explicit Sessions.Selection;
authorwenzelm
Fri Apr 07 10:47:25 2017 +0200 (2017-04-07)
changeset 65419457e4fbed731
parent 65417 fc41a5650fb1
child 65420 695d4e22345a
explicit Sessions.Selection;
Admin/jenkins/build/ci_build_benchmark.scala
Admin/jenkins/build/ci_build_makeall.scala
Admin/jenkins/build/ci_build_makeall_seq.scala
src/Pure/Admin/ci_profile.scala
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
src/Pure/Tools/ml_process.scala
     1.1 --- a/Admin/jenkins/build/ci_build_benchmark.scala	Thu Apr 06 21:37:13 2017 +0200
     1.2 +++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Apr 07 10:47:25 2017 +0200
     1.3 @@ -12,7 +12,6 @@
     1.4    def pre_hook(args: List[String]) = {}
     1.5    def post_hook(results: Build.Results) = {}
     1.6  
     1.7 -  def select_sessions(sessions: Sessions.T) =
     1.8 -    sessions.selection(session_groups = List("timing"))
     1.9 +  def selection = Sessions.Selection(session_groups = List("timing"))
    1.10  
    1.11  }
     2.1 --- a/Admin/jenkins/build/ci_build_makeall.scala	Thu Apr 06 21:37:13 2017 +0200
     2.2 +++ b/Admin/jenkins/build/ci_build_makeall.scala	Fri Apr 07 10:47:25 2017 +0200
     2.3 @@ -11,7 +11,6 @@
     2.4    def pre_hook(args: List[String]) = {}
     2.5    def post_hook(results: Build.Results) = {}
     2.6  
     2.7 -  def select_sessions(sessions: Sessions.T) =
     2.8 -    sessions.selection(all_sessions = true)
     2.9 +  def selection = Sessions.Selection(all_sessions = true)
    2.10  
    2.11  }
     3.1 --- a/Admin/jenkins/build/ci_build_makeall_seq.scala	Thu Apr 06 21:37:13 2017 +0200
     3.2 +++ b/Admin/jenkins/build/ci_build_makeall_seq.scala	Fri Apr 07 10:47:25 2017 +0200
     3.3 @@ -11,7 +11,6 @@
     3.4    def pre_hook(args: List[String]) = {}
     3.5    def post_hook(results: Build.Results) = {}
     3.6  
     3.7 -  def select_sessions(sessions: Sessions.T) =
     3.8 -    sessions.selection(all_sessions = true)
     3.9 +  def selection = Sessions.Selection(all_sessions = true)
    3.10  
    3.11  }
     4.1 --- a/src/Pure/Admin/ci_profile.scala	Thu Apr 06 21:37:13 2017 +0200
     4.2 +++ b/src/Pure/Admin/ci_profile.scala	Fri Apr 07 10:47:25 2017 +0200
     4.3 @@ -28,7 +28,7 @@
     4.4          dirs = include,
     4.5          select_dirs = select,
     4.6          system_mode = true,
     4.7 -        selection = select_sessions _)
     4.8 +        selection = selection)
     4.9      }
    4.10      val end_time = Time.now()
    4.11      (results, end_time - start_time)
    4.12 @@ -146,5 +146,5 @@
    4.13    def pre_hook(args: List[String]): Unit
    4.14    def post_hook(results: Build.Results): Unit
    4.15  
    4.16 -  def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
    4.17 +  def selection: Sessions.Selection
    4.18  }
     5.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 06 21:37:13 2017 +0200
     5.2 +++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 10:47:25 2017 +0200
     5.3 @@ -155,7 +155,8 @@
     5.4    def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
     5.5    {
     5.6      val full_sessions = load(options, dirs = dirs)
     5.7 -    val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
     5.8 +    val (_, selected_sessions) =
     5.9 +      full_sessions.selection(Selection(sessions = List(session)))
    5.10  
    5.11      deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
    5.12    }
    5.13 @@ -181,6 +182,57 @@
    5.14      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    5.15    }
    5.16  
    5.17 +  object Selection
    5.18 +  {
    5.19 +    val all: Selection = Selection(all_sessions = true)
    5.20 +  }
    5.21 +
    5.22 +  sealed case class Selection(
    5.23 +    requirements: Boolean = false,
    5.24 +    all_sessions: Boolean = false,
    5.25 +    exclude_session_groups: List[String] = Nil,
    5.26 +    exclude_sessions: List[String] = Nil,
    5.27 +    session_groups: List[String] = Nil,
    5.28 +    sessions: List[String] = Nil)
    5.29 +  {
    5.30 +    def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
    5.31 +    {
    5.32 +      val bad_sessions =
    5.33 +        SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
    5.34 +      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    5.35 +
    5.36 +      val excluded =
    5.37 +      {
    5.38 +        val exclude_group = exclude_session_groups.toSet
    5.39 +        val exclude_group_sessions =
    5.40 +          (for {
    5.41 +            (name, (info, _)) <- graph.iterator
    5.42 +            if graph.get_node(name).groups.exists(exclude_group)
    5.43 +          } yield name).toList
    5.44 +        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
    5.45 +      }
    5.46 +
    5.47 +      val pre_selected =
    5.48 +      {
    5.49 +        if (all_sessions) graph.keys
    5.50 +        else {
    5.51 +          val select_group = session_groups.toSet
    5.52 +          val select = sessions.toSet
    5.53 +          (for {
    5.54 +            (name, (info, _)) <- graph.iterator
    5.55 +            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
    5.56 +          } yield name).toList
    5.57 +        }
    5.58 +      }.filterNot(excluded)
    5.59 +
    5.60 +      val selected =
    5.61 +        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
    5.62 +        else pre_selected
    5.63 +
    5.64 +      (selected, graph.restrict(graph.all_preds(selected).toSet))
    5.65 +    }
    5.66 +  }
    5.67 +
    5.68    def make(infos: Traversable[(String, Info)]): T =
    5.69    {
    5.70      val graph1 =
    5.71 @@ -227,47 +279,9 @@
    5.72          name <- info.global_theories.iterator }
    5.73         yield name).toSet
    5.74  
    5.75 -    def selection(
    5.76 -      requirements: Boolean = false,
    5.77 -      all_sessions: Boolean = false,
    5.78 -      exclude_session_groups: List[String] = Nil,
    5.79 -      exclude_sessions: List[String] = Nil,
    5.80 -      session_groups: List[String] = Nil,
    5.81 -      sessions: List[String] = Nil): (List[String], T) =
    5.82 +    def selection(select: Selection): (List[String], T) =
    5.83      {
    5.84 -      val bad_sessions =
    5.85 -        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
    5.86 -      if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
    5.87 -
    5.88 -      val excluded =
    5.89 -      {
    5.90 -        val exclude_group = exclude_session_groups.toSet
    5.91 -        val exclude_group_sessions =
    5.92 -          (for {
    5.93 -            (name, (info, _)) <- graph.iterator
    5.94 -            if apply(name).groups.exists(exclude_group)
    5.95 -          } yield name).toList
    5.96 -        graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
    5.97 -      }
    5.98 -
    5.99 -      val pre_selected =
   5.100 -      {
   5.101 -        if (all_sessions) graph.keys
   5.102 -        else {
   5.103 -          val select_group = session_groups.toSet
   5.104 -          val select = sessions.toSet
   5.105 -          (for {
   5.106 -            (name, (info, _)) <- graph.iterator
   5.107 -            if info.select || select(name) || apply(name).groups.exists(select_group)
   5.108 -          } yield name).toList
   5.109 -        }
   5.110 -      }.filterNot(excluded)
   5.111 -
   5.112 -      val selected =
   5.113 -        if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
   5.114 -        else pre_selected
   5.115 -
   5.116 -      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
   5.117 +      val (selected, graph1) = select(graph)
   5.118        (selected, new T(graph1))
   5.119      }
   5.120  
     6.1 --- a/src/Pure/Tools/build.scala	Thu Apr 06 21:37:13 2017 +0200
     6.2 +++ b/src/Pure/Tools/build.scala	Fri Apr 07 10:47:25 2017 +0200
     6.3 @@ -368,9 +368,9 @@
     6.4        system_mode = system_mode,
     6.5        verbose = verbose,
     6.6        pide = pide,
     6.7 -      selection = { full_sessions =>
     6.8 -        full_sessions.selection(requirements, all_sessions,
     6.9 -          exclude_session_groups, exclude_sessions, session_groups, sessions) })
    6.10 +      selection =
    6.11 +        Sessions.Selection(requirements, all_sessions,
    6.12 +          exclude_session_groups, exclude_sessions, session_groups, sessions))
    6.13    }
    6.14  
    6.15    def build_selection(
    6.16 @@ -388,14 +388,13 @@
    6.17        system_mode: Boolean = false,
    6.18        verbose: Boolean = false,
    6.19        pide: Boolean = false,
    6.20 -      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
    6.21 -    ): Results =
    6.22 +      selection: Sessions.Selection = Sessions.Selection.all): Results =
    6.23    {
    6.24      /* session selection and dependencies */
    6.25  
    6.26      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
    6.27      val full_sessions = Sessions.load(build_options, dirs, select_dirs)
    6.28 -    val (selected, selected_sessions) = selection(full_sessions)
    6.29 +    val (selected, selected_sessions) = full_sessions.selection(selection)
    6.30      val deps =
    6.31        Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
    6.32          verbose = verbose, list_files = list_files, check_keywords = check_keywords,
     7.1 --- a/src/Pure/Tools/ml_process.scala	Thu Apr 06 21:37:13 2017 +0200
     7.2 +++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 10:47:25 2017 +0200
     7.3 @@ -30,8 +30,9 @@
     7.4      val heaps: List[String] =
     7.5        if (raw_ml_system) Nil
     7.6        else {
     7.7 +        val selection = Sessions.Selection(sessions = List(logic_name))
     7.8          val (_, selected_sessions) =
     7.9 -          sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
    7.10 +          sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
    7.11          (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
    7.12            map(a => File.platform_path(store.heap(a)))
    7.13        }