src/Pure/Tools/build.scala
changeset 56668 56335a8e2e8b
parent 56667 65e84b0ef974
child 56779 9823818588fb
equal deleted inserted replaced
56667:65e84b0ef974 56668:56335a8e2e8b
   421 
   421 
   422   def dependencies(progress: Progress, inlined_files: Boolean,
   422   def dependencies(progress: Progress, inlined_files: Boolean,
   423       verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   423       verbose: Boolean, list_files: Boolean, tree: Session_Tree): Deps =
   424     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   424     Deps((Map.empty[String, Session_Content] /: tree.topological_order)(
   425       { case (deps, (name, info)) =>
   425       { case (deps, (name, info)) =>
       
   426           if (progress.stopped) throw Exn.Interrupt()
       
   427 
   426           try {
   428           try {
   427             val (preloaded, parent_syntax) =
   429             val (preloaded, parent_syntax) =
   428               info.parent match {
   430               info.parent match {
   429                 case None =>
   431                 case None =>
   430                   (Set.empty[String], Outer_Syntax.init())
   432                   (Set.empty[String], Outer_Syntax.init())