src/Pure/Tools/build_cluster.scala
changeset 78964 a2de1f6ff94e
parent 78963 30360ee939f4
child 78965 890783dc4bc6
equal deleted inserted replaced
78963:30360ee939f4 78964:a2de1f6ff94e
    71             else error("Missing \":\" after host name")
    71             else error("Missing \":\" after host name")
    72           Options.Spec.parse(str.substring(l))
    72           Options.Spec.parse(str.substring(l))
    73         }
    73         }
    74         catch { case ERROR(msg) => err(msg) }
    74         catch { case ERROR(msg) => err(msg) }
    75 
    75 
    76       for (name <- space_explode(',', names)) yield {
    76       def get_registry(a: String): Registry.Cluster.A =
    77         val base_specs = Registry.Host.get(registry, name)
    77         Registry.Cluster.try_unqualify(a) match {
       
    78           case Some(b) => Registry.Cluster.get(registry, b)
       
    79           case None => List(a -> Registry.Host.get(registry, a))
       
    80         }
       
    81 
       
    82       for (name <- space_explode(',', names); (host, host_specs) <- get_registry(name))
       
    83       yield {
    78         val (params, options) =
    84         val (params, options) =
    79           try {
    85           try {
    80             val (specs1, specs2) = (base_specs ::: more_specs).partition(is_parameter)
    86             val (specs1, specs2) = (host_specs ::: more_specs).partition(is_parameter)
    81             (parameters ++ specs1, { test_options ++ specs2; specs2 })
    87             (parameters ++ specs1, { test_options ++ specs2; specs2 })
    82           }
    88           }
    83           catch { case ERROR(msg) => err(msg) }
    89           catch { case ERROR(msg) => err(msg) }
    84 
    90 
    85         apply(name = name,
    91         apply(name = host,
    86           hostname = params.string(HOSTNAME),
    92           hostname = params.string(HOSTNAME),
    87           user = params.string(USER),
    93           user = params.string(USER),
    88           port = params.int(PORT),
    94           port = params.int(PORT),
    89           jobs = params.int(JOBS),
    95           jobs = params.int(JOBS),
    90           numa = params.bool(NUMA),
    96           numa = params.bool(NUMA),