src/Pure/System/build.scala
changeset 48903 1621b3f26095
parent 48883 04cd2fddb4d9
child 48904 eaf240e9bdc8
equal deleted inserted replaced
48902:44a6967240b7 48903:1621b3f26095
   326     def is_empty: Boolean = deps.isEmpty
   326     def is_empty: Boolean = deps.isEmpty
   327     def apply(name: String): Session_Content = deps(name)
   327     def apply(name: String): Session_Content = deps(name)
   328     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   328     def sources(name: String): List[SHA1.Digest] = deps(name).sources.map(_._2)
   329   }
   329   }
   330 
   330 
   331   def dependencies(verbose: Boolean, tree: Session_Tree): Deps =
   331   def dependencies(verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   332     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   332     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   333       { case (deps, (name, info)) =>
   333       { case (deps, (name, info)) =>
   334           val (preloaded, parent_syntax, parent_errors) =
   334           val (preloaded, parent_syntax, parent_errors) =
   335             info.parent match {
   335             info.parent match {
   336               case None =>
   336               case None =>
   339                 val parent = deps(parent_name)
   339                 val parent = deps(parent_name)
   340                 (parent.loaded_theories, parent.syntax, parent.errors)
   340                 (parent.loaded_theories, parent.syntax, parent.errors)
   341             }
   341             }
   342           val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   342           val thy_info = new Thy_Info(new Thy_Load(preloaded, parent_syntax))
   343 
   343 
   344           if (verbose) {
   344           if (verbose || list_files) {
   345             val groups =
   345             val groups =
   346               if (info.groups.isEmpty) ""
   346               if (info.groups.isEmpty) ""
   347               else info.groups.mkString(" (", " ", ")")
   347               else info.groups.mkString(" (", " ", ")")
   348             echo("Session " + name + groups)
   348             echo("Session " + name + groups)
   349           }
   349           }
   360             thy_deps.deps.map({ case (n, h) =>
   360             thy_deps.deps.map({ case (n, h) =>
   361               val thy = Path.explode(n.node).expand
   361               val thy = Path.explode(n.node).expand
   362               val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   362               val uses = h.uses.map(p => (Path.explode(n.dir) + Path.explode(p._1)).expand)
   363               thy :: uses
   363               thy :: uses
   364             }).flatten ::: info.files.map(file => info.dir + file)
   364             }).flatten ::: info.files.map(file => info.dir + file)
       
   365 
       
   366           if (list_files)
       
   367             echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
       
   368 
   365           val sources =
   369           val sources =
   366             try { all_files.map(p => (p, SHA1.digest(p))) }
   370             try { all_files.map(p => (p, SHA1.digest(p))) }
   367             catch {
   371             catch {
   368               case ERROR(msg) =>
   372               case ERROR(msg) =>
   369                 error(msg + "\nThe error(s) above occurred in session " +
   373                 error(msg + "\nThe error(s) above occurred in session " +
   376 
   380 
   377   def session_content(dirs: List[Path], session: String): Session_Content =
   381   def session_content(dirs: List[Path], session: String): Session_Content =
   378   {
   382   {
   379     val (_, tree) =
   383     val (_, tree) =
   380       find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
   384       find_sessions(Options.init(), dirs.map((false, _))).required(false, Nil, List(session))
   381     dependencies(false, tree)(session)
   385     dependencies(false, false, tree)(session)
   382   }
   386   }
   383 
   387 
   384   def outer_syntax(session: String): Outer_Syntax =
   388   def outer_syntax(session: String): Outer_Syntax =
   385     session_content(Nil, session).check_errors.syntax
   389     session_content(Nil, session).check_errors.syntax
   386 
   390 
   529     build_heap: Boolean = false,
   533     build_heap: Boolean = false,
   530     clean_build: Boolean = false,
   534     clean_build: Boolean = false,
   531     more_dirs: List[(Boolean, Path)] = Nil,
   535     more_dirs: List[(Boolean, Path)] = Nil,
   532     session_groups: List[String] = Nil,
   536     session_groups: List[String] = Nil,
   533     max_jobs: Int = 1,
   537     max_jobs: Int = 1,
       
   538     list_files: Boolean = false,
   534     no_build: Boolean = false,
   539     no_build: Boolean = false,
   535     build_options: List[String] = Nil,
   540     build_options: List[String] = Nil,
   536     system_mode: Boolean = false,
   541     system_mode: Boolean = false,
   537     verbose: Boolean = false,
   542     verbose: Boolean = false,
   538     sessions: List[String] = Nil): Int =
   543     sessions: List[String] = Nil): Int =
   539   {
   544   {
   540     val options = (Options.init() /: build_options)(_ + _)
   545     val options = (Options.init() /: build_options)(_ + _)
   541     val (descendants, tree) =
   546     val (descendants, tree) =
   542       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   547       find_sessions(options, more_dirs).required(all_sessions, session_groups, sessions)
   543     val deps = dependencies(verbose, tree)
   548     val deps = dependencies(verbose, list_files, tree)
   544     val queue = Queue(tree)
   549     val queue = Queue(tree)
   545 
   550 
   546     def make_stamp(name: String): String =
   551     def make_stamp(name: String): String =
   547       sources_stamp(tree(name).entry_digest :: deps.sources(name))
   552       sources_stamp(tree(name).entry_digest :: deps.sources(name))
   548 
   553 
   690         case
   695         case
   691           Properties.Value.Boolean(all_sessions) ::
   696           Properties.Value.Boolean(all_sessions) ::
   692           Properties.Value.Boolean(build_heap) ::
   697           Properties.Value.Boolean(build_heap) ::
   693           Properties.Value.Boolean(clean_build) ::
   698           Properties.Value.Boolean(clean_build) ::
   694           Properties.Value.Int(max_jobs) ::
   699           Properties.Value.Int(max_jobs) ::
       
   700           Properties.Value.Boolean(list_files) ::
   695           Properties.Value.Boolean(no_build) ::
   701           Properties.Value.Boolean(no_build) ::
   696           Properties.Value.Boolean(system_mode) ::
   702           Properties.Value.Boolean(system_mode) ::
   697           Properties.Value.Boolean(verbose) ::
   703           Properties.Value.Boolean(verbose) ::
   698           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   704           Command_Line.Chunks(select_dirs, include_dirs, session_groups, build_options, sessions) =>
   699             val dirs =
   705             val dirs =
   700               select_dirs.map(d => (true, Path.explode(d))) :::
   706               select_dirs.map(d => (true, Path.explode(d))) :::
   701               include_dirs.map(d => (false, Path.explode(d)))
   707               include_dirs.map(d => (false, Path.explode(d)))
   702             build(all_sessions, build_heap, clean_build, dirs, session_groups,
   708             build(all_sessions, build_heap, clean_build, dirs, session_groups,
   703               max_jobs, no_build, build_options, system_mode, verbose, sessions)
   709               max_jobs, list_files, no_build, build_options, system_mode, verbose, sessions)
   704         case _ => error("Bad arguments:\n" + cat_lines(args))
   710         case _ => error("Bad arguments:\n" + cat_lines(args))
   705       }
   711       }
   706     }
   712     }
   707   }
   713   }
   708 }
   714 }