--- 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"))
}
--- 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)
}
--- 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)
}
--- 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
}
--- 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))
}
--- 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,
--- 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)))
}