src/Pure/Thy/sessions.scala
changeset 67024 72d37a2e9cca
parent 67023 e27e05d6f2a7
child 67025 961285f581e6
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 15:45:33 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 15:50:36 2017 +0100
     1.3 @@ -175,7 +175,7 @@
     1.4        }
     1.5    }
     1.6  
     1.7 -  def deps(sessions: T,
     1.8 +  def deps(sessions_structure: T,
     1.9        global_theories: Map[String, String],
    1.10        progress: Progress = No_Progress,
    1.11        inlined_files: Boolean = false,
    1.12 @@ -203,11 +203,11 @@
    1.13      }
    1.14  
    1.15      val session_bases =
    1.16 -      (Map.empty[String, Base] /: sessions.imports_topological_order)({
    1.17 +      (Map.empty[String, Base] /: sessions_structure.imports_topological_order)({
    1.18          case (session_bases, session_name) =>
    1.19            if (progress.stopped) throw Exn.Interrupt()
    1.20  
    1.21 -          val info = sessions(session_name)
    1.22 +          val info = sessions_structure(session_name)
    1.23            try {
    1.24              val parent_base: Sessions.Base =
    1.25                info.parent match {
    1.26 @@ -273,7 +273,8 @@
    1.27                }
    1.28  
    1.29                val imports_subgraph =
    1.30 -                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
    1.31 +                sessions_structure.imports_graph.
    1.32 +                  restrict(sessions_structure.imports_graph.all_preds(info.deps).toSet)
    1.33  
    1.34                val graph0 =
    1.35                  (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
    1.36 @@ -329,7 +330,7 @@
    1.37  
    1.38    sealed case class Base_Info(
    1.39      session: String,
    1.40 -    sessions: T,
    1.41 +    sessions_structure: T,
    1.42      errors: List[String],
    1.43      base: Base,
    1.44      infos: List[Info])