src/Pure/Tools/build.scala
changeset 56890 7f120d227ca5
parent 56873 f7c793b7fe7d
child 57923 cdae2467311d
     1.1 --- a/src/Pure/Tools/build.scala	Tue May 06 23:35:24 2014 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Wed May 07 10:13:31 2014 +0200
     1.3 @@ -288,7 +288,8 @@
     1.4      if (is_session_dir(dir)) dir
     1.5      else error("Bad session root directory: " + dir.toString)
     1.6  
     1.7 -  def find_sessions(options: Options, more_dirs: List[(Boolean, Path)]): Session_Tree =
     1.8 +  def find_sessions(options: Options, dirs: List[Path] = Nil, select_dirs: List[Path] = Nil)
     1.9 +    : Session_Tree =
    1.10    {
    1.11      def find_dir(select: Boolean, dir: Path): List[(String, Session_Info)] =
    1.12        find_root(select, dir) ::: find_roots(select, dir)
    1.13 @@ -320,13 +321,13 @@
    1.14        else Nil
    1.15      }
    1.16  
    1.17 -    val default_dirs = Isabelle_System.components().filter(is_session_dir(_)).map((false, _))
    1.18 -
    1.19 -    more_dirs foreach { case (_, dir) => check_session_dir(dir) }
    1.20 +    val default_dirs = Isabelle_System.components().filter(is_session_dir(_))
    1.21 +    dirs.foreach(check_session_dir(_))
    1.22 +    select_dirs.foreach(check_session_dir(_))
    1.23  
    1.24      Session_Tree(
    1.25        for {
    1.26 -        (select, dir) <- default_dirs ::: more_dirs
    1.27 +        (select, dir) <- (default_dirs ::: dirs).map((false, _)) ::: select_dirs.map((true, _))
    1.28          info <- find_dir(select, dir)
    1.29        } yield info)
    1.30    }
    1.31 @@ -511,8 +512,7 @@
    1.32      dirs: List[Path],
    1.33      sessions: List[String]): Deps =
    1.34    {
    1.35 -    val (_, tree) =
    1.36 -      find_sessions(options, dirs.map((false, _))).selection(false, false, Nil, sessions)
    1.37 +    val (_, tree) = find_sessions(options, dirs = dirs).selection(false, false, Nil, sessions)
    1.38      dependencies(Ignore_Progress, inlined_files, false, false, tree)
    1.39    }
    1.40  
    1.41 @@ -722,7 +722,8 @@
    1.42      all_sessions: Boolean = false,
    1.43      build_heap: Boolean = false,
    1.44      clean_build: Boolean = false,
    1.45 -    more_dirs: List[(Boolean, Path)] = Nil,
    1.46 +    dirs: List[Path] = Nil,
    1.47 +    select_dirs: List[Path] = Nil,
    1.48      session_groups: List[String] = Nil,
    1.49      max_jobs: Int = 1,
    1.50      list_files: Boolean = false,
    1.51 @@ -733,7 +734,7 @@
    1.52    {
    1.53      /* session tree and dependencies */
    1.54  
    1.55 -    val full_tree = find_sessions(options, more_dirs)
    1.56 +    val full_tree = find_sessions(options, dirs, select_dirs)
    1.57      val (selected, selected_tree) =
    1.58        full_tree.selection(requirements, all_sessions, session_groups, sessions)
    1.59  
    1.60 @@ -972,7 +973,8 @@
    1.61      all_sessions: Boolean = false,
    1.62      build_heap: Boolean = false,
    1.63      clean_build: Boolean = false,
    1.64 -    more_dirs: List[(Boolean, Path)] = Nil,
    1.65 +    dirs: List[Path] = Nil,
    1.66 +    select_dirs: List[Path] = Nil,
    1.67      session_groups: List[String] = Nil,
    1.68      max_jobs: Int = 1,
    1.69      list_files: Boolean = false,
    1.70 @@ -983,8 +985,8 @@
    1.71    {
    1.72      val results =
    1.73        build_results(options, progress, requirements, all_sessions,
    1.74 -        build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
    1.75 -        system_mode, verbose, sessions)
    1.76 +        build_heap, clean_build, dirs, select_dirs, session_groups, max_jobs,
    1.77 +        list_files, no_build, system_mode, verbose, sessions)
    1.78  
    1.79      val rc = (0 /: results)({ case (rc1, (_, rc2)) => rc1 max rc2 })
    1.80      if (rc != 0 && (verbose || !no_build)) {
    1.81 @@ -1012,16 +1014,13 @@
    1.82            Properties.Value.Boolean(no_build) ::
    1.83            Properties.Value.Boolean(system_mode) ::
    1.84            Properties.Value.Boolean(verbose) ::
    1.85 -          Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
    1.86 +          Command_Line.Chunks(dirs, select_dirs, session_groups, build_options, sessions) =>
    1.87              val options = (Options.init() /: build_options)(_ + _)
    1.88 -            val more_dirs =
    1.89 -              select_dirs.map(d => (true, Path.explode(d))) :::
    1.90 -              include_dirs.map(d => (false, Path.explode(d)))
    1.91              val progress = new Console_Progress(verbose)
    1.92              progress.interrupt_handler {
    1.93 -              build(options, progress, requirements, all_sessions,
    1.94 -                build_heap, clean_build, more_dirs, session_groups, max_jobs, list_files, no_build,
    1.95 -                system_mode, verbose, sessions)
    1.96 +              build(options, progress, requirements, all_sessions, build_heap, clean_build,
    1.97 +                dirs.map(Path.explode(_)), select_dirs.map(Path.explode(_)), session_groups,
    1.98 +                max_jobs, list_files, no_build, system_mode, verbose, sessions)
    1.99              }
   1.100          case _ => error("Bad arguments:\n" + cat_lines(args))
   1.101        }