# HG changeset patch # User wenzelm # Date 1342634515 -7200 # Node ID 752de4e10162dbe0ee77400f8ae9a45137c4363a # Parent 6f4fc030882a9db6e34fc47f65df9f731bb9728c tuned source structure; diff -r 6f4fc030882a -r 752de4e10162 src/Pure/System/build.scala --- a/src/Pure/System/build.scala Wed Jul 18 19:47:10 2012 +0200 +++ b/src/Pure/System/build.scala Wed Jul 18 20:01:55 2012 +0200 @@ -15,64 +15,6 @@ object Build { - /* command line entry point */ - - private object Bool - { - def unapply(s: String): Option[Boolean] = - s match { - case "true" => Some(true) - case "false" => Some(false) - case _ => None - } - } - - private object Chunks - { - private def chunks(list: List[String]): List[List[String]] = - list.indexWhere(_ == "\n") match { - case -1 => List(list) - case i => - val (chunk, rest) = list.splitAt(i) - chunk :: chunks(rest.tail) - } - def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) - } - - def main(args: Array[String]) - { - val rc = - try { - args.toList match { - case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: - Chunks(more_dirs, options, sessions) => - build(all_sessions, build_images, list_only, - more_dirs.map(Path.explode), options, sessions) - case _ => error("Bad arguments:\n" + cat_lines(args)) - } - } - catch { - case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 - } - sys.exit(rc) - } - - - /* build */ - - def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean, - more_dirs: List[Path], options: List[String], sessions: List[String]): Int = - { - println("more_dirs = " + more_dirs.toString) - println("options = " + options.toString) - println("sessions = " + sessions.toString) - - find_sessions(more_dirs) foreach println - - 0 - } - - /** session information **/ type Options = List[(String, Option[String])] @@ -152,7 +94,7 @@ } - /* find session */ + /* find sessions */ def find_sessions(more_dirs: List[Path]): List[Session_Info] = { @@ -199,5 +141,65 @@ } infos.toList } + + + + /** build **/ + + def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean, + more_dirs: List[Path], options: List[String], sessions: List[String]): Int = + { + println("more_dirs = " + more_dirs.toString) + println("options = " + options.toString) + println("sessions = " + sessions.toString) + + find_sessions(more_dirs) foreach println + + 0 + } + + + + /** command line entry point **/ + + private object Bool + { + def unapply(s: String): Option[Boolean] = + s match { + case "true" => Some(true) + case "false" => Some(false) + case _ => None + } + } + + private object Chunks + { + private def chunks(list: List[String]): List[List[String]] = + list.indexWhere(_ == "\n") match { + case -1 => List(list) + case i => + val (chunk, rest) = list.splitAt(i) + chunk :: chunks(rest.tail) + } + def unapplySeq(list: List[String]): Option[List[List[String]]] = Some(chunks(list)) + } + + def main(args: Array[String]) + { + val rc = + try { + args.toList match { + case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: + Chunks(more_dirs, options, sessions) => + build(all_sessions, build_images, list_only, + more_dirs.map(Path.explode), options, sessions) + case _ => error("Bad arguments:\n" + cat_lines(args)) + } + } + catch { + case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2 + } + sys.exit(rc) + } }