src/Pure/System/build.scala
changeset 48351 a0b95a762abb
parent 48350 09bf3b73e446
child 48352 7fbf98ee265f
equal deleted inserted replaced
48350:09bf3b73e446 48351:a0b95a762abb
    38       override def toString: String = name
    38       override def toString: String = name
    39     }
    39     }
    40 
    40 
    41     sealed case class Info(
    41     sealed case class Info(
    42       dir: Path,
    42       dir: Path,
    43       key: Key,
       
    44       parent: Option[String],
       
    45       description: String,
    43       description: String,
    46       options: Options,
    44       options: Options,
    47       theories: List[(Options, String)],
    45       theories: List[(Options, String)],
    48       files: List[String])
    46       files: List[String])
    49     {
       
    50       def name: String = key.name
       
    51     }
       
    52 
    47 
    53     object Queue
    48     object Queue
    54     {
    49     {
    55       val empty: Queue = new Queue()
    50       val empty: Queue = new Queue()
    56     }
    51     }
    57 
    52 
    58     final class Queue private(
    53     final class Queue private(
    59       keys: Map[String, Key] = Map.empty,
    54       keys: Map[String, Key] = Map.empty,
    60       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    55       graph: Graph[Key, Info] = Graph.empty(Key.Ordering))
    61     {
    56     {
    62       def lookup(name: String): Option[Info] =
    57       def defined(name: String): Boolean = keys.isDefinedAt(name)
    63         keys.get(name).map(graph.get_node(_))
    58 
    64 
    59       def + (key: Key, info: Info, parent: Option[String]): Queue =
    65       def + (info: Info): Queue =
       
    66       {
    60       {
    67         val keys1 =
    61         val keys1 =
    68           if (keys.isDefinedAt(info.name)) error("Duplicate session: " + quote(info.name))
    62           if (defined(key.name)) error("Duplicate session: " + quote(key.name))
    69           else keys + (info.name -> info.key)
    63           else keys + (key.name -> key)
    70 
    64 
    71         val graph1 =
    65         val graph1 =
    72           try {
    66           try {
    73             graph.new_node(info.key, info).
    67             graph.new_node(key, info).add_deps_acyclic(key, parent.toList.map(keys(_)))
    74               add_deps_acyclic(info.key, info.parent.toList.map(keys(_)))
       
    75           }
    68           }
    76           catch {
    69           catch {
    77             case exn: Graph.Cycles[_] =>
    70             case exn: Graph.Cycles[_] =>
    78               error(cat_lines(exn.cycles.map(cycle =>
    71               error(cat_lines(exn.cycles.map(cycle =>
    79                 "Cyclic session dependency of " +
    72                 "Cyclic session dependency of " +
    80                   cycle.map(key => quote(key.toString)).mkString(" via "))))
    73                   cycle.map(key => quote(key.toString)).mkString(" via "))))
    81           }
    74           }
    82         new Queue(keys1, graph1)
    75         new Queue(keys1, graph1)
    83       }
    76       }
    84 
    77 
    85       def topological_order: List[Info] =
    78       def topological_order: List[(Key, Info)] =
    86         graph.topological_order.map(graph.get_node(_))
    79         graph.topological_order.map(key => (key, graph.get_node(key)))
    87     }
    80     }
    88   }
    81   }
    89 
    82 
    90 
    83 
    91   /* parsing */
    84   /* parsing */
   174             if (entry.parent.isDefined) error("Illegal parent session")
   167             if (entry.parent.isDefined) error("Illegal parent session")
   175             else entry.name
   168             else entry.name
   176           }
   169           }
   177           else
   170           else
   178             entry.parent match {
   171             entry.parent match {
   179               case None => error("Missing parent session")
   172               case Some(parent_name) if sessions.defined(parent_name) =>
   180               case Some(parent) =>
       
   181                 val parent_info =
       
   182                   sessions.lookup(parent) getOrElse
       
   183                     error("Undefined parent session: " + quote(parent))
       
   184                 if (entry.reset) entry.name
   173                 if (entry.reset) entry.name
   185                 else parent_info.name + "-" + entry.name
   174                 else parent_name + "-" + entry.name
       
   175               case _ => error("Bad parent session")
   186             }
   176             }
   187 
   177 
   188         val path =
   178         val path =
   189           entry.path match {
   179           entry.path match {
   190             case Some(p) => Path.explode(p)
   180             case Some(p) => Path.explode(p)
   191             case None => Path.basic(entry.name)
   181             case None => Path.basic(entry.name)
   192           }
   182           }
   193         val thys = entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten
   183 
   194         val info =
   184         val key = Session.Key(full_name, entry.order)
   195           Session.Info(dir + path, Session.Key(full_name, entry.order),
   185         val info = Session.Info(dir + path, entry.description, entry.options,
   196             entry.parent, entry.description, entry.options, thys, entry.files)
   186           entry.theories.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, entry.files)
   197 
   187 
   198         sessions += info
   188         sessions += (key, info, entry.parent)
   199       }
   189       }
   200       catch {
   190       catch {
   201         case ERROR(msg) =>
   191         case ERROR(msg) =>
   202           error(msg + "\nThe error(s) above occurred in session entry " +
   192           error(msg + "\nThe error(s) above occurred in session entry " +
   203             quote(entry.name) + " (file " + quote(root.toString) + ")")
   193             quote(entry.name) + " (file " + quote(root.toString) + ")")
   215   {
   205   {
   216     println("more_dirs = " + more_dirs.toString)
   206     println("more_dirs = " + more_dirs.toString)
   217     println("options = " + options.toString)
   207     println("options = " + options.toString)
   218     println("sessions = " + sessions.toString)
   208     println("sessions = " + sessions.toString)
   219 
   209 
   220     for (info <- find_sessions(more_dirs).topological_order)
   210     for ((key, info) <- find_sessions(more_dirs).topological_order)
   221       println(info.name + " in " + info.dir)
   211       println(key.name + " in " + info.dir)
   222 
   212 
   223     0
   213     0
   224   }
   214   }
   225 
   215 
   226 
   216