--- a/src/Pure/Admin/afp.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/Admin/afp.scala Tue Nov 07 21:46:28 2017 +0100
@@ -36,8 +36,8 @@
val sessions: List[String] = entries.flatMap(_.sessions)
val sessions_structure: Sessions.T =
- Sessions.load(options, dirs = List(main_dir)).
- selection(Sessions.Selection(sessions = sessions.toList))._2
+ Sessions.load_structure(options, dirs = List(main_dir)).
+ selection(Sessions.Selection(sessions = sessions.toList))
/* dependency graph */
--- a/src/Pure/Admin/build_doc.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/Admin/build_doc.scala Tue Nov 07 21:46:28 2017 +0100
@@ -22,13 +22,15 @@
system_mode: Boolean = false,
docs: List[String] = Nil): Int =
{
+ val sessions_structure = Sessions.load_structure(options)
val selection =
for {
- info <- Sessions.load(options).build_topological_order
+ name <- sessions_structure.build_topological_order
+ info = sessions_structure(name)
if info.groups.contains("doc")
doc = info.options.string("document_variants")
if all_docs || docs.contains(doc)
- } yield (doc, info.name)
+ } yield (doc, name)
val selected_docs = selection.map(_._1)
val sessions = selection.map(_._2)
--- a/src/Pure/ML/ml_process.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/ML/ml_process.scala Tue Nov 07 21:46:28 2017 +0100
@@ -32,8 +32,8 @@
if (raw_ml_system) Nil
else {
val selection = Sessions.Selection(sessions = List(logic_name))
- val (_, selected_sessions) =
- sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
+ val selected_sessions =
+ sessions.getOrElse(Sessions.load_structure(options, dirs = dirs)).selection(selection)
selected_sessions.build_requirements(List(logic_name)).
map(a => File.platform_path(store.heap(a)))
}
--- a/src/Pure/Thy/sessions.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/Thy/sessions.scala Tue Nov 07 21:46:28 2017 +0100
@@ -175,7 +175,7 @@
}
}
- def deps(sessions: T,
+ def deps(sessions_structure: T,
global_theories: Map[String, String],
progress: Progress = No_Progress,
inlined_files: Boolean = false,
@@ -203,10 +203,11 @@
}
val session_bases =
- (Map.empty[String, Base] /: sessions.imports_topological_order)({
- case (session_bases, info) =>
+ (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
+ case (session_bases, session_name) =>
if (progress.stopped) throw Exn.Interrupt()
+ val info = sessions_structure(session_name)
try {
val parent_base: Sessions.Base =
info.parent match {
@@ -272,7 +273,8 @@
}
val imports_subgraph =
- sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
+ sessions_structure.imports_graph.
+ restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet)
val graph0 =
(Graph_Display.empty_graph /: imports_subgraph.topological_order)(
@@ -328,7 +330,7 @@
sealed case class Base_Info(
session: String,
- sessions: T,
+ sessions_structure: T,
errors: List[String],
base: Base,
infos: List[Info])
@@ -343,11 +345,11 @@
focus_session: Boolean = false,
required_session: Boolean = false): Base_Info =
{
- val full_sessions = load(options, dirs = dirs)
+ val full_sessions = load_structure(options, dirs = dirs)
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
@@ -398,13 +400,13 @@
val full_sessions1 =
if (infos1.isEmpty) full_sessions
- else load(options, dirs = dirs, infos = infos1)
+ else load_structure(options, dirs = dirs, infos = infos1)
val select_sessions1 =
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)
@@ -509,43 +511,34 @@
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]) =
+ def selected(graph: Graph[String, Info]): List[String] =
{
- 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 select_group = session_groups.toSet
+ val select_session = sessions.toSet ++ graph.all_succs(base_sessions)
- val excluded =
- {
- val exclude_group = exclude_session_groups.toSet
- val exclude_group_sessions =
+ val selected0 =
+ if (all_sessions) graph.keys
+ else {
(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)
+ if info.dir_selected || select_session(name) ||
+ graph.get_node(name).groups.exists(select_group)
} yield name).toList
}
- }.filterNot(excluded)
+
+ if (requirements) (graph.all_preds(selected0).toSet -- selected0).toList
+ else selected0
+ }
- 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 excluded(graph: Graph[String, Info]): List[String] =
+ {
+ 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)
}
}
@@ -594,9 +587,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 /:
@@ -613,26 +606,34 @@
}
})
- 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 = sel.excluded(build_graph).toSet
+
+ def restrict(graph: Graph[String, Info]): Graph[String, Info] =
+ {
+ val sessions = graph.all_preds(sel.selected(graph)).filterNot(excluded)
+ graph.restrict(graph.all_preds(sessions).toSet)
+ }
+
+ new T(restrict(build_graph), restrict(imports_graph))
}
- def build_descendants(names: List[String]): List[String] =
- build_graph.all_succs(names)
- def build_requirements(names: List[String]): List[String] =
- build_graph.all_preds(names).reverse
- def build_topological_order: List[Info] =
- build_graph.topological_order.map(apply(_))
+ def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
+ def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
+ def build_requirements(ss: List[String]): List[String] = build_graph.all_preds(ss).reverse
+ def build_topological_order: List[String] = build_graph.topological_order
- def imports_descendants(names: List[String]): List[String] =
- imports_graph.all_succs(names)
- def imports_requirements(names: List[String]): List[String] =
- imports_graph.all_preds(names).reverse
- def imports_topological_order: List[Info] =
- imports_graph.topological_order.map(apply(_))
+ def imports_selection(sel: Selection): List[String] = sel.selected(imports_graph)
+ def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
+ def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds(ss).reverse
+ def imports_topological_order: List[String] = imports_graph.topological_order
override def toString: String =
imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
@@ -784,7 +785,7 @@
(default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
}
- def load(options: Options,
+ def load_structure(options: Options,
dirs: List[Path] = Nil,
select_dirs: List[Path] = Nil,
infos: List[Info] = Nil): T =
--- a/src/Pure/Tools/build.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/Tools/build.scala Tue Nov 07 21:46:28 2017 +0100
@@ -382,7 +382,7 @@
/* session selection and dependencies */
val full_sessions =
- Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
+ Sessions.load_structure(build_options, dirs = dirs, select_dirs = select_dirs, infos = infos)
def sources_stamp(deps: Sessions.Deps, name: String): String =
{
@@ -391,13 +391,13 @@
SHA1.digest(cat_lines(digests.map(_.toString).sorted)).toString
}
- val (selected, selected_sessions, deps) =
+ val selection1 =
+ Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
+ exclude_sessions, session_groups, sessions) ++ selection
+
+ val (selected_sessions, deps) =
{
- val (selected0, selected_sessions0) =
- full_sessions.selection(
- Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
- exclude_sessions, session_groups, sessions) ++ selection)
-
+ val selected_sessions0 = full_sessions.selection(selection1)
val deps0 =
Sessions.deps(selected_sessions0, full_sessions.global_theories,
progress = progress, inlined_files = true, verbose = verbose,
@@ -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(full_sessions.build_selection(selection1))) {
val files =
List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
map(store.output_dir + _).filter(_.is_file)
--- a/src/Pure/Tools/imports.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Pure/Tools/imports.scala Tue Nov 07 21:46:28 2017 +0100
@@ -99,8 +99,8 @@
select_dirs: List[Path] = Nil,
verbose: Boolean = false) =
{
- val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
- val (selected, selected_sessions) = full_sessions.selection(selection)
+ val full_sessions = Sessions.load_structure(options, dirs = dirs, select_dirs = select_dirs)
+ 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.map(_.name).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(info =>
- {
- imports(options, operation_update = operation_update, progress = progress,
- update_message = " for session " + quote(info.name),
- selection = Sessions.Selection(sessions = List(info.name)),
- dirs = dirs ::: select_dirs, verbose = verbose)
- })
+ Sessions.load_structure(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)
+ })
}
})
}
--- a/src/Tools/jEdit/src/jedit_sessions.scala Tue Nov 07 15:16:42 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Tue Nov 07 21:46:28 2017 +0100
@@ -45,7 +45,10 @@
def logic_parent: Boolean = Isabelle_System.getenv("JEDIT_LOGIC_PARENT") == "true"
def logic_info(options: Options): Option[Sessions.Info] =
- try { Sessions.load(session_options(options), dirs = session_dirs()).get(logic_name(options)) }
+ try {
+ Sessions.load_structure(session_options(options), dirs = session_dirs()).
+ get(logic_name(options))
+ }
catch { case ERROR(_) => None }
def logic_root(options: Options): Position.T =
@@ -68,10 +71,11 @@
val session_list =
{
- val sessions = Sessions.load(options.value, dirs = session_dirs())
+ val sessions_structure = Sessions.load_structure(options.value, dirs = session_dirs())
val (main_sessions, other_sessions) =
- sessions.imports_topological_order.partition(info => info.groups.contains("main"))
- main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
+ sessions_structure.imports_topological_order.
+ partition(name => sessions_structure(name).groups.contains("main"))
+ main_sessions.sorted ::: other_sessions.sorted
}
val entries =
@@ -129,7 +133,7 @@
def session_start(options: Options)
{
Isabelle_Process.start(PIDE.session, session_options(options),
- sessions = Some(PIDE.resources.session_base_info.sessions),
+ sessions = Some(PIDE.resources.session_base_info.sessions_structure),
logic = PIDE.resources.session_name,
store = Sessions.store(session_build_mode() == "system"),
modes =