tuned;
authorwenzelm
Tue Oct 31 17:03:57 2017 +0100 (18 months ago)
changeset 66961f855f9aed72f
parent 66960 d62f1f03868a
child 66962 e1bde71bace6
tuned;
src/Pure/ML/ml_process.scala
src/Pure/Tools/build.scala
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/ML/ml_process.scala	Tue Oct 31 16:42:20 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_process.scala	Tue Oct 31 17:03:57 2017 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4        else {
     1.5          val selection = Sessions.Selection(sessions = List(logic_name))
     1.6          val (_, selected_sessions) =
     1.7 -          sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
     1.8 +          sessions.getOrElse(Sessions.load(options, dirs = dirs)).selection(selection)
     1.9          selected_sessions.build_requirements(List(logic_name)).
    1.10            map(a => File.platform_path(store.heap(a)))
    1.11        }
     2.1 --- a/src/Pure/Tools/build.scala	Tue Oct 31 16:42:20 2017 +0100
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 31 17:03:57 2017 +0100
     2.3 @@ -380,7 +380,8 @@
     2.4  
     2.5      /* session selection and dependencies */
     2.6  
     2.7 -    val full_sessions = Sessions.load(build_options, dirs, select_dirs)
     2.8 +    val full_sessions =
     2.9 +      Sessions.load(build_options, dirs = dirs, select_dirs = select_dirs)
    2.10  
    2.11      def sources_stamp(deps: Sessions.Deps, name: String): String =
    2.12      {
     3.1 --- a/src/Pure/Tools/imports.scala	Tue Oct 31 16:42:20 2017 +0100
     3.2 +++ b/src/Pure/Tools/imports.scala	Tue Oct 31 17:03:57 2017 +0100
     3.3 @@ -99,7 +99,7 @@
     3.4      select_dirs: List[Path] = Nil,
     3.5      verbose: Boolean = false) =
     3.6    {
     3.7 -    val full_sessions = Sessions.load(options, dirs, select_dirs)
     3.8 +    val full_sessions = Sessions.load(options, dirs = dirs, select_dirs = select_dirs)
     3.9      val (selected, selected_sessions) = full_sessions.selection(selection)
    3.10  
    3.11      val deps =
    3.12 @@ -313,7 +313,7 @@
    3.13        }
    3.14        else if (operation_update && incremental_update) {
    3.15          val (selected, selected_sessions) =
    3.16 -          Sessions.load(options, dirs, select_dirs).selection(selection)
    3.17 +          Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
    3.18          selected_sessions.imports_topological_order.foreach(info =>
    3.19          {
    3.20            imports(options, operation_update = operation_update, progress = progress,