src/Pure/Thy/sessions.scala
changeset 67052 caf87d4b9b61
parent 67029 d6d9fd2559ce
child 67053 57c37ee49c39
     1.1 --- a/src/Pure/Thy/sessions.scala	Sat Nov 11 18:41:08 2017 +0000
     1.2 +++ b/src/Pure/Thy/sessions.scala	Sun Nov 12 12:41:05 2017 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  def deps(sessions_structure: T,
     1.8 +  def deps(sessions_structure: Structure,
     1.9        global_theories: Map[String, String],
    1.10        progress: Progress = No_Progress,
    1.11        inlined_files: Boolean = false,
    1.12 @@ -330,7 +330,7 @@
    1.13  
    1.14    sealed case class Base_Info(
    1.15      session: String,
    1.16 -    sessions_structure: T,
    1.17 +    sessions_structure: Structure,
    1.18      errors: List[String],
    1.19      base: Base,
    1.20      infos: List[Info])
    1.21 @@ -542,7 +542,7 @@
    1.22      }
    1.23    }
    1.24  
    1.25 -  def make(infos: List[Info]): T =
    1.26 +  def make(infos: List[Info]): Structure =
    1.27    {
    1.28      def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
    1.29        : Graph[String, Info] =
    1.30 @@ -577,10 +577,10 @@
    1.31      val graph1 = add_edges(graph0, "parent", _.parent)
    1.32      val graph2 = add_edges(graph1, "imports", _.imports)
    1.33  
    1.34 -    new T(graph1, graph2)
    1.35 +    new Structure(graph1, graph2)
    1.36    }
    1.37  
    1.38 -  final class T private[Sessions](
    1.39 +  final class Structure private[Sessions](
    1.40        val build_graph: Graph[String, Info],
    1.41        val imports_graph: Graph[String, Info])
    1.42    {
    1.43 @@ -606,7 +606,7 @@
    1.44                }
    1.45            })
    1.46  
    1.47 -    def selection(sel: Selection): T =
    1.48 +    def selection(sel: Selection): Structure =
    1.49      {
    1.50        val bad_sessions =
    1.51          SortedSet((sel.base_sessions ::: sel.exclude_sessions ::: sel.sessions).
    1.52 @@ -622,7 +622,7 @@
    1.53          graph.restrict(graph.all_preds(sessions).toSet)
    1.54        }
    1.55  
    1.56 -      new T(restrict(build_graph), restrict(imports_graph))
    1.57 +      new Structure(restrict(build_graph), restrict(imports_graph))
    1.58      }
    1.59  
    1.60      def build_selection(sel: Selection): List[String] = sel.selected(build_graph)
    1.61 @@ -636,7 +636,7 @@
    1.62      def imports_topological_order: List[String] = imports_graph.topological_order
    1.63  
    1.64      override def toString: String =
    1.65 -      imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
    1.66 +      imports_graph.keys_iterator.mkString("Sessions.Structure(", ", ", ")")
    1.67    }
    1.68  
    1.69  
    1.70 @@ -788,7 +788,7 @@
    1.71    def load_structure(options: Options,
    1.72      dirs: List[Path] = Nil,
    1.73      select_dirs: List[Path] = Nil,
    1.74 -    infos: List[Info] = Nil): T =
    1.75 +    infos: List[Info] = Nil): Structure =
    1.76    {
    1.77      def load_dir(select: Boolean, dir: Path): List[(Boolean, Path)] =
    1.78        load_root(select, dir) ::: load_roots(select, dir)