src/Pure/Tools/build.scala
changeset 65251 4b0a43afc3fb
parent 65250 13a6c81534a8
child 65253 85c0ac5c2589
     1.1 --- a/src/Pure/Tools/build.scala	Wed Mar 15 10:08:27 2017 +0100
     1.2 +++ b/src/Pure/Tools/build.scala	Wed Mar 15 10:31:42 2017 +0100
     1.3 @@ -93,119 +93,6 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* source dependencies and static content */
     1.8 -
     1.9 -  sealed case class Deps(deps: Map[String, Sessions.Base])
    1.10 -  {
    1.11 -    def is_empty: Boolean = deps.isEmpty
    1.12 -    def apply(name: String): Sessions.Base = deps(name)
    1.13 -    def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
    1.14 -  }
    1.15 -
    1.16 -  def dependencies(
    1.17 -      progress: Progress = No_Progress,
    1.18 -      inlined_files: Boolean = false,
    1.19 -      verbose: Boolean = false,
    1.20 -      list_files: Boolean = false,
    1.21 -      check_keywords: Set[String] = Set.empty,
    1.22 -      tree: Sessions.Tree): Deps =
    1.23 -    Deps((Map.empty[String, Sessions.Base] /: tree.topological_order)(
    1.24 -      { case (deps, (name, info)) =>
    1.25 -          if (progress.stopped) throw Exn.Interrupt()
    1.26 -
    1.27 -          try {
    1.28 -            val resources =
    1.29 -              new Resources(
    1.30 -                info.parent match {
    1.31 -                  case None => Sessions.Base.bootstrap
    1.32 -                  case Some(parent) => deps(parent)
    1.33 -                })
    1.34 -
    1.35 -            if (verbose || list_files) {
    1.36 -              val groups =
    1.37 -                if (info.groups.isEmpty) ""
    1.38 -                else info.groups.mkString(" (", " ", ")")
    1.39 -              progress.echo("Session " + info.chapter + "/" + name + groups)
    1.40 -            }
    1.41 -
    1.42 -            val thy_deps =
    1.43 -            {
    1.44 -              val root_theories =
    1.45 -                info.theories.flatMap({
    1.46 -                  case (global, _, thys) =>
    1.47 -                    thys.map(thy =>
    1.48 -                      (resources.node_name(
    1.49 -                        if (global) "" else name, info.dir + resources.thy_path(thy)), info.pos))
    1.50 -                })
    1.51 -              val thy_deps = resources.thy_info.dependencies(name, root_theories)
    1.52 -
    1.53 -              thy_deps.errors match {
    1.54 -                case Nil => thy_deps
    1.55 -                case errs => error(cat_lines(errs))
    1.56 -              }
    1.57 -            }
    1.58 -
    1.59 -            val known_theories =
    1.60 -              (resources.base.known_theories /: thy_deps.deps)({ case (known, dep) =>
    1.61 -                val name = dep.name
    1.62 -                known.get(name.theory) match {
    1.63 -                  case Some(name1) if name != name1 =>
    1.64 -                    error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
    1.65 -                  case _ =>
    1.66 -                    known + (name.theory -> name) + (Long_Name.base_name(name.theory) -> name)
    1.67 -                }
    1.68 -              })
    1.69 -
    1.70 -            val loaded_theories = thy_deps.loaded_theories
    1.71 -            val keywords = thy_deps.keywords
    1.72 -            val syntax = thy_deps.syntax
    1.73 -
    1.74 -            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    1.75 -            val loaded_files =
    1.76 -              if (inlined_files) {
    1.77 -                val pure_files =
    1.78 -                  if (Sessions.pure_name(name)) Sessions.pure_files(resources, syntax, info.dir)
    1.79 -                  else Nil
    1.80 -                pure_files ::: thy_deps.loaded_files
    1.81 -              }
    1.82 -              else Nil
    1.83 -
    1.84 -            val all_files =
    1.85 -              (theory_files ::: loaded_files :::
    1.86 -                info.files.map(file => info.dir + file) :::
    1.87 -                info.document_files.map(file => info.dir + file._1 + file._2)).map(_.expand)
    1.88 -
    1.89 -            if (list_files)
    1.90 -              progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
    1.91 -
    1.92 -            if (check_keywords.nonEmpty)
    1.93 -              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
    1.94 -
    1.95 -            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
    1.96 -
    1.97 -            val session_graph =
    1.98 -              Present.session_graph(info.parent getOrElse "",
    1.99 -                resources.base.loaded_theories, thy_deps.deps)
   1.100 -
   1.101 -            val base =
   1.102 -              Sessions.Base(
   1.103 -                loaded_theories, known_theories, keywords, syntax, sources, session_graph)
   1.104 -            deps + (name -> base)
   1.105 -          }
   1.106 -          catch {
   1.107 -            case ERROR(msg) =>
   1.108 -              cat_error(msg, "The error(s) above occurred in session " +
   1.109 -                quote(name) + Position.here(info.pos))
   1.110 -          }
   1.111 -      }))
   1.112 -
   1.113 -  def session_base(options: Options, session: String, dirs: List[Path] = Nil): Sessions.Base =
   1.114 -  {
   1.115 -    val (_, tree) = Sessions.load(options, dirs = dirs).selection(sessions = List(session))
   1.116 -    dependencies(tree = tree)(session)
   1.117 -  }
   1.118 -
   1.119 -
   1.120    /* jobs */
   1.121  
   1.122    private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
   1.123 @@ -431,7 +318,8 @@
   1.124      val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
   1.125      val full_tree = Sessions.load(build_options, dirs, select_dirs)
   1.126      val (selected, selected_tree) = selection(full_tree)
   1.127 -    val deps = dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   1.128 +    val deps =
   1.129 +      Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
   1.130  
   1.131      def session_sources_stamp(name: String): String =
   1.132        sources_stamp(selected_tree(name).meta_digest :: deps.sources(name))