src/Pure/Thy/sessions.scala
changeset 67026 687c822ee5e3
parent 67025 961285f581e6
child 67027 d4f245bea081
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Nov 07 16:44:25 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 16:50:26 2017 +0100
     1.3 @@ -345,7 +345,7 @@
     1.4      focus_session: Boolean = false,
     1.5      required_session: Boolean = false): Base_Info =
     1.6    {
     1.7 -    val full_sessions = load(options, dirs = dirs)
     1.8 +    val full_sessions = load_structure(options, dirs = dirs)
     1.9      val global_theories = full_sessions.global_theories
    1.10  
    1.11      val selected_sessions =
    1.12 @@ -400,7 +400,7 @@
    1.13  
    1.14      val full_sessions1 =
    1.15        if (infos1.isEmpty) full_sessions
    1.16 -      else load(options, dirs = dirs, infos = infos1)
    1.17 +      else load_structure(options, dirs = dirs, infos = infos1)
    1.18  
    1.19      val select_sessions1 =
    1.20        if (focus_session) full_sessions1.imports_descendants(List(session1))
    1.21 @@ -784,7 +784,7 @@
    1.22      (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.23    }
    1.24  
    1.25 -  def load(options: Options,
    1.26 +  def load_structure(options: Options,
    1.27      dirs: List[Path] = Nil,
    1.28      select_dirs: List[Path] = Nil,
    1.29      infos: List[Info] = Nil): T =