removed unused option, which is potentially expensive;
authorwenzelm
Tue Oct 31 22:17:38 2017 +0100 (19 months ago)
changeset 6696939077839947e
parent 66968 9991671c98aa
child 66970 13857f49d215
removed unused option, which is potentially expensive;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Tue Oct 31 21:50:09 2017 +0100
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 22:17:38 2017 +0100
     1.3 @@ -330,7 +330,6 @@
     1.4      session: String,
     1.5      dirs: List[Path] = Nil,
     1.6      infos: List[Info] = Nil,
     1.7 -    inlined_files: Boolean = false,
     1.8      all_known: Boolean = false,
     1.9      required_session: Boolean = false): Base_Info =
    1.10    {
    1.11 @@ -339,7 +338,7 @@
    1.12      val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
    1.13  
    1.14      val sessions: T = if (all_known) full_sessions else selected_sessions
    1.15 -    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
    1.16 +    val deps = Sessions.deps(sessions, global_theories)
    1.17      val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
    1.18  
    1.19      val other_session: Option[(String, List[Info])] =
    1.20 @@ -385,8 +384,8 @@
    1.21      other_session match {
    1.22        case None => new Base_Info(session, sessions, deps, base, infos)
    1.23        case Some((other_name, more_infos)) =>
    1.24 -        session_base_info(options, other_name, dirs = dirs, infos = more_infos ::: infos,
    1.25 -          inlined_files = inlined_files, all_known = all_known)
    1.26 +        session_base_info(options, other_name,
    1.27 +          dirs = dirs, infos = more_infos ::: infos, all_known = all_known)
    1.28      }
    1.29    }
    1.30