# HG changeset patch # User wenzelm # Date 1510486865 -3600 # Node ID caf87d4b9b6125e14d3f34acdbc176719a762abf # Parent e7e54a0b9197aa002dcdcafef8588a76d7613767 tuned signature; diff -r e7e54a0b9197 -r caf87d4b9b61 src/Pure/Admin/afp.scala --- a/src/Pure/Admin/afp.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/Admin/afp.scala Sun Nov 12 12:41:05 2017 +0100 @@ -35,7 +35,7 @@ val sessions: List[String] = entries.flatMap(_.sessions) - val sessions_structure: Sessions.T = + val sessions_structure: Sessions.Structure = Sessions.load_structure(options, dirs = List(main_dir)). selection(Sessions.Selection(sessions = sessions.toList)) diff -r e7e54a0b9197 -r caf87d4b9b61 src/Pure/ML/ml_process.scala --- a/src/Pure/ML/ml_process.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/ML/ml_process.scala Sun Nov 12 12:41:05 2017 +0100 @@ -23,7 +23,7 @@ redirect: Boolean = false, cleanup: () => Unit = () => (), channel: Option[System_Channel] = None, - sessions: Option[Sessions.T] = None, + sessions: Option[Sessions.Structure] = None, session_base: Option[Sessions.Base] = None, store: Sessions.Store = Sessions.store()): Bash.Process = { diff -r e7e54a0b9197 -r caf87d4b9b61 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/System/isabelle_process.scala Sun Nov 12 12:41:05 2017 +0100 @@ -20,7 +20,7 @@ modes: List[String] = Nil, cwd: JFile = null, env: Map[String, String] = Isabelle_System.settings(), - sessions: Option[Sessions.T] = None, + sessions: Option[Sessions.Structure] = None, store: Sessions.Store = Sessions.store(), phase_changed: Session.Phase => Unit = null) { @@ -43,7 +43,7 @@ env: Map[String, String] = Isabelle_System.settings(), receiver: Prover.Receiver = Console.println(_), xml_cache: XML.Cache = new XML.Cache(), - sessions: Option[Sessions.T] = None, + sessions: Option[Sessions.Structure] = None, store: Sessions.Store = Sessions.store()): Prover = { val channel = System_Channel() diff -r e7e54a0b9197 -r caf87d4b9b61 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/Thy/sessions.scala Sun Nov 12 12:41:05 2017 +0100 @@ -175,7 +175,7 @@ } } - def deps(sessions_structure: T, + def deps(sessions_structure: Structure, global_theories: Map[String, String], progress: Progress = No_Progress, inlined_files: Boolean = false, @@ -330,7 +330,7 @@ sealed case class Base_Info( session: String, - sessions_structure: T, + sessions_structure: Structure, errors: List[String], base: Base, infos: List[Info]) @@ -542,7 +542,7 @@ } } - def make(infos: List[Info]): T = + def make(infos: List[Info]): Structure = { def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String]) : Graph[String, Info] = @@ -577,10 +577,10 @@ val graph1 = add_edges(graph0, "parent", _.parent) val graph2 = add_edges(graph1, "imports", _.imports) - new T(graph1, graph2) + new Structure(graph1, graph2) } - final class T private[Sessions]( + final class Structure private[Sessions]( val build_graph: Graph[String, Info], val imports_graph: Graph[String, Info]) { @@ -606,7 +606,7 @@ } }) - def selection(sel: Selection): T = + def selection(sel: Selection): Structure = { val bad_sessions = SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions). @@ -622,7 +622,7 @@ graph.restrict(graph.all_preds(sessions).toSet) } - new T(restrict(build_graph), restrict(imports_graph)) + new Structure(restrict(build_graph), restrict(imports_graph)) } def build_selection(sel: Selection): List[String] = sel.selected(build_graph) @@ -636,7 +636,7 @@ def imports_topological_order: List[String] = imports_graph.topological_order override def toString: String = - imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")") + imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")") } @@ -788,7 +788,7 @@ def load_structure(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil, - infos: List[Info] = Nil): T = + infos: List[Info] = Nil): Structure = { def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] = load_root(select, dir) ::: load_roots(select, dir) diff -r e7e54a0b9197 -r caf87d4b9b61 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Sat Nov 11 18:41:08 2017 +0000 +++ b/src/Pure/Tools/build.scala Sun Nov 12 12:41:05 2017 +0100 @@ -71,7 +71,7 @@ } } - def apply(progress: Progress, sessions: Sessions.T, store: Sessions.Store): Queue = + def apply(progress: Progress, sessions: Sessions.Structure, store: Sessions.Store): Queue = { val graph = sessions.build_graph val names = graph.keys @@ -178,7 +178,7 @@ private class Job(progress: Progress, name: String, val info: Sessions.Info, - sessions: Sessions.T, + sessions: Sessions.Structure, deps: Sessions.Deps, store: Sessions.Store, do_output: Boolean,