src/Pure/Tools/build.scala
changeset 68204 a554da2811f2
parent 68198 6710167e17af
child 68209 aeffd8f1f079
     1.1 --- a/src/Pure/Tools/build.scala	Thu May 17 14:50:48 2018 +0200
     1.2 +++ b/src/Pure/Tools/build.scala	Thu May 17 15:38:36 2018 +0200
     1.3 @@ -174,7 +174,6 @@
     1.4    private class Job(progress: Progress,
     1.5      name: String,
     1.6      val info: Sessions.Info,
     1.7 -    sessions: Sessions.Structure,
     1.8      deps: Sessions.Deps,
     1.9      store: Sessions.Store,
    1.10      do_output: Boolean,
    1.11 @@ -238,8 +237,8 @@
    1.12  
    1.13            val session_result = Future.promise[Process_Result]
    1.14  
    1.15 -          Isabelle_Process.start(session, options, logic = parent,
    1.16 -            cwd = info.dir.file, env = env, sessions = Some(sessions), store = store,
    1.17 +          Isabelle_Process.start(session, options, logic = parent, cwd = info.dir.file, env = env,
    1.18 +            sessions_structure = Some(deps.sessions_structure), store = store,
    1.19              phase_changed =
    1.20              {
    1.21                case Session.Ready => session.protocol_command("build_session", args_yxml)
    1.22 @@ -272,12 +271,12 @@
    1.23                  args =
    1.24                    (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
    1.25                    List("--eval", eval),
    1.26 -                env = env, sessions = Some(sessions), store = store,
    1.27 +                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
    1.28                  cleanup = () => args_file.delete)
    1.29              }
    1.30              else {
    1.31                ML_Process(options, parent, List("--eval", eval), cwd = info.dir.file,
    1.32 -                env = env, sessions = Some(sessions), store = store,
    1.33 +                env = env, sessions_structure = Some(deps.sessions_structure), store = store,
    1.34                  cleanup = () => args_file.delete)
    1.35              }
    1.36  
    1.37 @@ -413,17 +412,16 @@
    1.38        Sessions.Selection(requirements, all_sessions, base_sessions, exclude_session_groups,
    1.39          exclude_sessions, session_groups, sessions) ++ selection
    1.40  
    1.41 -    val (selected_sessions, deps) =
    1.42 +    val deps =
    1.43      {
    1.44 -      val selected_sessions0 = full_sessions.selection(selection1)
    1.45        val deps0 =
    1.46 -        Sessions.deps(selected_sessions0, full_sessions.global_theories,
    1.47 +        Sessions.deps(full_sessions.selection(selection1), full_sessions.global_theories,
    1.48            progress = progress, inlined_files = true, verbose = verbose,
    1.49            list_files = list_files, check_keywords = check_keywords).check_errors
    1.50  
    1.51        if (soft_build && !fresh_build) {
    1.52          val outdated =
    1.53 -          selected_sessions0.build_topological_order.flatMap(name =>
    1.54 +          deps0.sessions_structure.build_topological_order.flatMap(name =>
    1.55              store.find_database(name) match {
    1.56                case Some(database) =>
    1.57                  using(SQLite.open_database(database))(store.read_build(_, name)) match {
    1.58 @@ -433,14 +431,11 @@
    1.59                  }
    1.60                case None => Some(name)
    1.61              })
    1.62 -        val selected_sessions =
    1.63 -          full_sessions.selection(Sessions.Selection(sessions = outdated))
    1.64 -        val deps =
    1.65 -          Sessions.deps(selected_sessions, full_sessions.global_theories,
    1.66 -            progress = progress, inlined_files = true).check_errors
    1.67 -        (selected_sessions, deps)
    1.68 +
    1.69 +        Sessions.deps(full_sessions.selection(Sessions.Selection(sessions = outdated)),
    1.70 +          full_sessions.global_theories, progress = progress, inlined_files = true).check_errors
    1.71        }
    1.72 -      else (selected_sessions0, deps0)
    1.73 +      else deps0
    1.74      }
    1.75  
    1.76  
    1.77 @@ -465,7 +460,7 @@
    1.78  
    1.79      /* main build process */
    1.80  
    1.81 -    val queue = Queue(progress, selected_sessions, store)
    1.82 +    val queue = Queue(progress, deps.sessions_structure, store)
    1.83  
    1.84      store.prepare_output()
    1.85  
    1.86 @@ -592,7 +587,7 @@
    1.87              pending.dequeue(running.isDefinedAt(_)) match {
    1.88                case Some((name, info)) =>
    1.89                  val ancestor_results =
    1.90 -                  selected_sessions.build_requirements(List(name)).filterNot(_ == name).
    1.91 +                  deps.sessions_structure.build_requirements(List(name)).filterNot(_ == name).
    1.92                      map(results(_))
    1.93                  val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
    1.94  
    1.95 @@ -636,7 +631,7 @@
    1.96  
    1.97                    val numa_node = numa_nodes.next(used_node(_))
    1.98                    val job =
    1.99 -                    new Job(progress, name, info, selected_sessions, deps, store, do_output,
   1.100 +                    new Job(progress, name, info, deps, store, do_output,
   1.101                        verbose, pide, numa_node, queue.command_timings(name))
   1.102                    loop(pending, running + (name -> (ancestor_heaps, job)), results)
   1.103                  }