# HG changeset patch # User wenzelm # Date 1491554845 -7200 # Node ID 457e4fbed73179cdabdd71bac01a3c796ef172d7 # Parent fc41a5650fb1af9cfa93346bd4200a3fe547a572 explicit Sessions.Selection; diff -r fc41a5650fb1 -r 457e4fbed731 Admin/jenkins/build/ci_build_benchmark.scala --- a/Admin/jenkins/build/ci_build_benchmark.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/Admin/jenkins/build/ci_build_benchmark.scala Fri Apr 07 10:47:25 2017 +0200 @@ -12,7 +12,6 @@ def pre_hook(args: List[String]) = {} def post_hook(results: Build.Results) = {} - def select_sessions(sessions: Sessions.T) = - sessions.selection(session_groups = List("timing")) + def selection = Sessions.Selection(session_groups = List("timing")) } diff -r fc41a5650fb1 -r 457e4fbed731 Admin/jenkins/build/ci_build_makeall.scala --- a/Admin/jenkins/build/ci_build_makeall.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/Admin/jenkins/build/ci_build_makeall.scala Fri Apr 07 10:47:25 2017 +0200 @@ -11,7 +11,6 @@ def pre_hook(args: List[String]) = {} def post_hook(results: Build.Results) = {} - def select_sessions(sessions: Sessions.T) = - sessions.selection(all_sessions = true) + def selection = Sessions.Selection(all_sessions = true) } diff -r fc41a5650fb1 -r 457e4fbed731 Admin/jenkins/build/ci_build_makeall_seq.scala --- a/Admin/jenkins/build/ci_build_makeall_seq.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/Admin/jenkins/build/ci_build_makeall_seq.scala Fri Apr 07 10:47:25 2017 +0200 @@ -11,7 +11,6 @@ def pre_hook(args: List[String]) = {} def post_hook(results: Build.Results) = {} - def select_sessions(sessions: Sessions.T) = - sessions.selection(all_sessions = true) + def selection = Sessions.Selection(all_sessions = true) } diff -r fc41a5650fb1 -r 457e4fbed731 src/Pure/Admin/ci_profile.scala --- a/src/Pure/Admin/ci_profile.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/src/Pure/Admin/ci_profile.scala Fri Apr 07 10:47:25 2017 +0200 @@ -28,7 +28,7 @@ dirs = include, select_dirs = select, system_mode = true, - selection = select_sessions _) + selection = selection) } val end_time = Time.now() (results, end_time - start_time) @@ -146,5 +146,5 @@ def pre_hook(args: List[String]): Unit def post_hook(results: Build.Results): Unit - def select_sessions(sessions: Sessions.T): (List[String], Sessions.T) + def selection: Sessions.Selection } diff -r fc41a5650fb1 -r 457e4fbed731 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/src/Pure/Thy/sessions.scala Fri Apr 07 10:47:25 2017 +0200 @@ -155,7 +155,8 @@ def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base = { val full_sessions = load(options, dirs = dirs) - val (_, selected_sessions) = full_sessions.selection(sessions = List(session)) + val (_, selected_sessions) = + full_sessions.selection(Selection(sessions = List(session))) deps(selected_sessions, global_theories = full_sessions.global_theories)(session) } @@ -181,6 +182,57 @@ def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale")) } + object Selection + { + val all: Selection = Selection(all_sessions = true) + } + + sealed case class Selection( + requirements: Boolean = false, + all_sessions: Boolean = false, + exclude_session_groups: List[String] = Nil, + exclude_sessions: List[String] = Nil, + session_groups: List[String] = Nil, + sessions: List[String] = Nil) + { + def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) = + { + val bad_sessions = + SortedSet((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 + (for { + (name, (info, _)) <- graph.iterator + if info.select || 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: Traversable[(String, Info)]): T = { val graph1 = @@ -227,47 +279,9 @@ name <- info.global_theories.iterator } yield name).toSet - def selection( - requirements: Boolean = false, - all_sessions: Boolean = false, - exclude_session_groups: List[String] = Nil, - exclude_sessions: List[String] = Nil, - session_groups: List[String] = Nil, - sessions: List[String] = Nil): (List[String], T) = + def selection(select: Selection): (List[String], T) = { - val bad_sessions = - SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).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 apply(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 - (for { - (name, (info, _)) <- graph.iterator - if info.select || select(name) || apply(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 - - val graph1 = graph.restrict(graph.all_preds(selected).toSet) + val (selected, graph1) = select(graph) (selected, new T(graph1)) } diff -r fc41a5650fb1 -r 457e4fbed731 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/src/Pure/Tools/build.scala Fri Apr 07 10:47:25 2017 +0200 @@ -368,9 +368,9 @@ system_mode = system_mode, verbose = verbose, pide = pide, - selection = { full_sessions => - full_sessions.selection(requirements, all_sessions, - exclude_session_groups, exclude_sessions, session_groups, sessions) }) + selection = + Sessions.Selection(requirements, all_sessions, + exclude_session_groups, exclude_sessions, session_groups, sessions)) } def build_selection( @@ -388,14 +388,13 @@ system_mode: Boolean = false, verbose: Boolean = false, pide: Boolean = false, - selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true)) - ): Results = + selection: Sessions.Selection = Sessions.Selection.all): Results = { /* session selection and dependencies */ val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true) val full_sessions = Sessions.load(build_options, dirs, select_dirs) - val (selected, selected_sessions) = selection(full_sessions) + val (selected, selected_sessions) = full_sessions.selection(selection) val deps = Sessions.deps(selected_sessions, progress = progress, inlined_files = true, verbose = verbose, list_files = list_files, check_keywords = check_keywords, diff -r fc41a5650fb1 -r 457e4fbed731 src/Pure/Tools/ml_process.scala --- a/src/Pure/Tools/ml_process.scala Thu Apr 06 21:37:13 2017 +0200 +++ b/src/Pure/Tools/ml_process.scala Fri Apr 07 10:47:25 2017 +0200 @@ -30,8 +30,9 @@ val heaps: List[String] = if (raw_ml_system) Nil else { + val selection = Sessions.Selection(sessions = List(logic_name)) val (_, selected_sessions) = - sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name)) + sessions.getOrElse(Sessions.load(options, dirs)).selection(selection) (selected_sessions.ancestors(logic_name) ::: List(logic_name)). map(a => File.platform_path(store.heap(a))) }