src/Pure/System/build.scala
changeset 49098 673e0ed547af
parent 48992 0518bf89c777
child 49131 aa1e2ba3c697
     1.1 --- a/src/Pure/System/build.scala	Mon Sep 03 20:57:51 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Mon Sep 03 21:30:34 2012 +0200
     1.3 @@ -331,7 +331,8 @@
     1.4      def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
     1.5    }
     1.6  
     1.7 -  def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
     1.8 +  def dependencies(inlined_files: Boolean, verbose: Boolean, list_files: Boolean,
     1.9 +      tree: Session_Tree): Deps =
    1.10      Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
    1.11        { case (deps, (name, info)) =>
    1.12            val (preloaded, parent_syntax, parent_errors) =
    1.13 @@ -352,7 +353,7 @@
    1.14            }
    1.15  
    1.16            val thy_deps =
    1.17 -            thy_info.dependencies(
    1.18 +            thy_info.dependencies(inlined_files,
    1.19                info.theories.map(_._2).flatten.
    1.20                  map(thy => Document.Node.Name(info.dir + Thy_Load.thy_path(thy))))
    1.21  
    1.22 @@ -381,15 +382,15 @@
    1.23            deps + (name -> Session_Content(loaded_theories, syntax, sources, errors))
    1.24        }))
    1.25  
    1.26 -  def session_content(dirs: List[Path], session: String): Session_Content =
    1.27 +  def session_content(inlined_files: Boolean, dirs: List[Path], session: String): Session_Content =
    1.28    {
    1.29      val (_, tree) =
    1.30        find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
    1.31 -    dependencies(false, false, tree)(session)
    1.32 +    dependencies(inlined_files, false, false, tree)(session)
    1.33    }
    1.34  
    1.35    def outer_syntax(session: String): Outer_Syntax =
    1.36 -    session_content(Nil, session).check_errors.syntax
    1.37 +    session_content(false, Nil, session).check_errors.syntax
    1.38  
    1.39  
    1.40    /* jobs */
    1.41 @@ -548,7 +549,7 @@
    1.42      val options = (Options.init() /: build_options)(_ + _)
    1.43      val (descendants, tree) =
    1.44        find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
    1.45 -    val deps = dependencies(verbose, list_files, tree)
    1.46 +    val deps = dependencies(true, verbose, list_files, tree)
    1.47      val queue = Queue(tree)
    1.48  
    1.49      def make_stamp(name: String): String =