src/Pure/System/build.scala
changeset 48341 752de4e10162
parent 48340 6f4fc030882a
child 48344 8dc904c45945
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 19:47:10 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 20:01:55 2012 +0200
     1.3 @@ -15,64 +15,6 @@
     1.4  
     1.5  object Build
     1.6  {
     1.7 -  /* command line entry point */
     1.8 -
     1.9 -  private object Bool
    1.10 -  {
    1.11 -    def unapply(s: String): Option[Boolean] =
    1.12 -      s match {
    1.13 -        case "true" => Some(true)
    1.14 -        case "false" => Some(false)
    1.15 -        case _ => None
    1.16 -      }
    1.17 -  }
    1.18 -
    1.19 -  private object Chunks
    1.20 -  {
    1.21 -    private def chunks(list: List[String]): List[List[String]] =
    1.22 -      list.indexWhere(_ == "\n") match {
    1.23 -        case -1 => List(list)
    1.24 -        case i =>
    1.25 -          val (chunk, rest) = list.splitAt(i)
    1.26 -          chunk :: chunks(rest.tail)
    1.27 -      }
    1.28 -    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
    1.29 -  }
    1.30 -
    1.31 -  def main(args: Array[String])
    1.32 -  {
    1.33 -    val rc =
    1.34 -      try {
    1.35 -        args.toList match {
    1.36 -          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
    1.37 -            Chunks(more_dirs, options, sessions) =>
    1.38 -              build(all_sessions, build_images, list_only,
    1.39 -                more_dirs.map(Path.explode), options, sessions)
    1.40 -          case _ => error("Bad arguments:\n" + cat_lines(args))
    1.41 -        }
    1.42 -      }
    1.43 -      catch {
    1.44 -        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
    1.45 -      }
    1.46 -    sys.exit(rc)
    1.47 -  }
    1.48 -
    1.49 -
    1.50 -  /* build */
    1.51 -
    1.52 -  def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    1.53 -    more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
    1.54 -  {
    1.55 -    println("more_dirs = " + more_dirs.toString)
    1.56 -    println("options = " + options.toString)
    1.57 -    println("sessions = " + sessions.toString)
    1.58 -
    1.59 -    find_sessions(more_dirs) foreach println
    1.60 -
    1.61 -    0
    1.62 -  }
    1.63 -
    1.64 -
    1.65    /** session information **/
    1.66  
    1.67    type Options = List[(String, Option[String])]
    1.68 @@ -152,7 +94,7 @@
    1.69    }
    1.70  
    1.71  
    1.72 -  /* find session */
    1.73 +  /* find sessions */
    1.74  
    1.75    def find_sessions(more_dirs: List[Path]): List[Session_Info] =
    1.76    {
    1.77 @@ -199,5 +141,65 @@
    1.78      }
    1.79      infos.toList
    1.80    }
    1.81 +
    1.82 +
    1.83 +
    1.84 +  /** build **/
    1.85 +
    1.86 +  def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    1.87 +    more_dirs: List[Path], options: List[String], sessions: List[String]): Int =
    1.88 +  {
    1.89 +    println("more_dirs = " + more_dirs.toString)
    1.90 +    println("options = " + options.toString)
    1.91 +    println("sessions = " + sessions.toString)
    1.92 +
    1.93 +    find_sessions(more_dirs) foreach println
    1.94 +
    1.95 +    0
    1.96 +  }
    1.97 +
    1.98 +
    1.99 +
   1.100 +  /** command line entry point **/
   1.101 +
   1.102 +  private object Bool
   1.103 +  {
   1.104 +    def unapply(s: String): Option[Boolean] =
   1.105 +      s match {
   1.106 +        case "true" => Some(true)
   1.107 +        case "false" => Some(false)
   1.108 +        case _ => None
   1.109 +      }
   1.110 +  }
   1.111 +
   1.112 +  private object Chunks
   1.113 +  {
   1.114 +    private def chunks(list: List[String]): List[List[String]] =
   1.115 +      list.indexWhere(_ == "\n") match {
   1.116 +        case -1 => List(list)
   1.117 +        case i =>
   1.118 +          val (chunk, rest) = list.splitAt(i)
   1.119 +          chunk :: chunks(rest.tail)
   1.120 +      }
   1.121 +    def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list))
   1.122 +  }
   1.123 +
   1.124 +  def main(args: Array[String])
   1.125 +  {
   1.126 +    val rc =
   1.127 +      try {
   1.128 +        args.toList match {
   1.129 +          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) ::
   1.130 +            Chunks(more_dirs, options, sessions) =>
   1.131 +              build(all_sessions, build_images, list_only,
   1.132 +                more_dirs.map(Path.explode), options, sessions)
   1.133 +          case _ => error("Bad arguments:\n" + cat_lines(args))
   1.134 +        }
   1.135 +      }
   1.136 +      catch {
   1.137 +        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
   1.138 +      }
   1.139 +    sys.exit(rc)
   1.140 +  }
   1.141  }
   1.142