# 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,