tuned signature;
authorwenzelm
Thu Apr 06 15:20:45 2017 +0200 (2017-04-06)
changeset 65406cc9e2f1f279d
parent 65405 68f8a0dab28b
child 65407 4546272431e9
tuned signature;
src/Pure/Thy/sessions.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Thu Apr 06 14:41:56 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Thu Apr 06 15:20:45 2017 +0200
     1.3 @@ -42,31 +42,30 @@
     1.4        loaded_theories.contains(name.theory)
     1.5    }
     1.6  
     1.7 -  sealed case class Deps(deps: Map[String, Base])
     1.8 +  sealed case class Deps(sessions: Map[String, Base])
     1.9    {
    1.10 -    def is_empty: Boolean = deps.isEmpty
    1.11 -    def apply(name: String): Base = deps(name)
    1.12 -    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    1.13 +    def is_empty: Boolean = sessions.isEmpty
    1.14 +    def apply(name: String): Base = sessions(name)
    1.15 +    def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
    1.16    }
    1.17  
    1.18 -  def dependencies(
    1.19 +  def deps(tree: Tree,
    1.20        progress: Progress = No_Progress,
    1.21        inlined_files: Boolean = false,
    1.22        verbose: Boolean = false,
    1.23        list_files: Boolean = false,
    1.24        check_keywords: Set[String] = Set.empty,
    1.25 -      global_theories: Set[String] = Set.empty,
    1.26 -      tree: Tree): Deps =
    1.27 +      global_theories: Set[String] = Set.empty): Deps =
    1.28    {
    1.29      Deps((Map.empty[String, Base] /: tree.topological_order)(
    1.30 -      { case (deps, (name, info)) =>
    1.31 +      { case (sessions, (name, info)) =>
    1.32            if (progress.stopped) throw Exn.Interrupt()
    1.33  
    1.34            try {
    1.35              val parent_base =
    1.36                info.parent match {
    1.37                  case None => Base.bootstrap
    1.38 -                case Some(parent) => deps(parent)
    1.39 +                case Some(parent) => sessions(parent)
    1.40                }
    1.41              val resources = new Resources(name, parent_base)
    1.42  
    1.43 @@ -142,7 +141,7 @@
    1.44                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.45                  session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
    1.46  
    1.47 -            deps + (name -> base)
    1.48 +            sessions + (name -> base)
    1.49            }
    1.50            catch {
    1.51              case ERROR(msg) =>
    1.52 @@ -157,7 +156,7 @@
    1.53      val full_tree = load(options, dirs = dirs)
    1.54      val (_, tree) = full_tree.selection(sessions = List(session))
    1.55  
    1.56 -    dependencies(global_theories = full_tree.global_theories, tree = tree)(session)
    1.57 +    deps(tree, global_theories = full_tree.global_theories)(session)
    1.58    }
    1.59  
    1.60  
     2.1 --- a/src/Pure/Tools/build.scala	Thu Apr 06 14:41:56 2017 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Thu Apr 06 15:20:45 2017 +0200
     2.3 @@ -395,9 +395,9 @@
     2.4      val full_tree = Sessions.load(build_options, dirs, select_dirs)
     2.5      val (selected, selected_tree) = selection(full_tree)
     2.6      val deps =
     2.7 -      Sessions.dependencies(
     2.8 -        progress, true, verbose, list_files, check_keywords,
     2.9 -          full_tree.global_theories, selected_tree)
    2.10 +      Sessions.deps(selected_tree, progress = progress, inlined_files = true,
    2.11 +        verbose = verbose, list_files = list_files, check_keywords = check_keywords,
    2.12 +        global_theories = full_tree.global_theories)
    2.13  
    2.14      def sources_stamp(name: String): List[String] =
    2.15        (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted