tuned;
authorwenzelm
Mon Mar 13 16:06:13 2017 +0100 (2017-03-13)
changeset 6521173ba79126b55
parent 65210 8cfdf420b643
child 65212 fd6bc719c98b
tuned;
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Tools/build.scala	Mon Mar 13 15:59:00 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Mon Mar 13 16:06:13 2017 +0100
     1.3 @@ -199,23 +199,10 @@
     1.4            }
     1.5        }))
     1.6  
     1.7 -  def session_dependencies(
     1.8 -    options: Options,
     1.9 -    inlined_files: Boolean,
    1.10 -    dirs: List[Path],
    1.11 -    sessions: List[String]): Deps =
    1.12 +  def session_base(options: Options, session: String, dirs: List[Path] = Nil): Sessions.Base =
    1.13    {
    1.14 -    val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = sessions)
    1.15 -    dependencies(inlined_files = inlined_files, tree = tree)
    1.16 -  }
    1.17 -
    1.18 -  def session_base(
    1.19 -    options: Options,
    1.20 -    session_name: String,
    1.21 -    session_dirs: List[Path] = Nil,
    1.22 -    inlined_files: Boolean = false): Sessions.Base =
    1.23 -  {
    1.24 -    session_dependencies(options, inlined_files, session_dirs, List(session_name))(session_name)
    1.25 +    val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = List(session))
    1.26 +    dependencies(tree = tree)(session)
    1.27    }
    1.28  
    1.29