src/Pure/System/build.scala
changeset 48335 2f923e994056
parent 48334 8dff9933e72a
child 48336 3c55bfad22eb
     1.1 --- a/src/Pure/System/build.scala	Wed Jul 18 13:43:36 2012 +0200
     1.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
     1.3 @@ -7,6 +7,9 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 +import java.io.File
     1.8 +
     1.9 +
    1.10  object Build
    1.11  {
    1.12    /* command line entry point */
    1.13 @@ -23,24 +26,27 @@
    1.14  
    1.15    def main(args: Array[String])
    1.16    {
    1.17 -    def bad_args()
    1.18 -    {
    1.19 -      java.lang.System.err.println("Bad arguments: " + args.toString)
    1.20 -      sys.exit(2)
    1.21 -    }
    1.22 +    def bad_args(): Nothing = error("Bad arguments: " + args.toString)
    1.23  
    1.24 -    args.toList match {
    1.25 -      case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
    1.26 -        rest.indexWhere(_ == "\n") match {
    1.27 -          case -1 => bad_args()
    1.28 -          case i =>
    1.29 -            val (options, rest1) = rest.splitAt(i)
    1.30 -            val sessions = rest1.tail
    1.31 -            val rc = build(all_sessions, build_images, list_only, options, sessions)
    1.32 -            sys.exit(rc)
    1.33 +    val rc =
    1.34 +      try {
    1.35 +        args.toList match {
    1.36 +          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
    1.37 +            rest.indexWhere(_ == "\n") match {
    1.38 +              case -1 => bad_args()
    1.39 +              case i =>
    1.40 +                val (options, rest1) = rest.splitAt(i)
    1.41 +                val sessions = rest1.tail
    1.42 +                build(all_sessions, build_images, list_only, options, sessions)
    1.43 +            }
    1.44 +          case _ => bad_args()
    1.45          }
    1.46 -      case _ => bad_args()
    1.47 -    }
    1.48 +      }
    1.49 +      catch {
    1.50 +        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
    1.51 +      }
    1.52 +
    1.53 +    sys.exit(rc)
    1.54    }
    1.55  
    1.56  
    1.57 @@ -49,12 +55,12 @@
    1.58    def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    1.59      options: List[String], sessions: List[String]): Int =
    1.60    {
    1.61 -    val rc = 1
    1.62 -
    1.63      println("options = " + options.toString)
    1.64      println("sessions = " + sessions.toString)
    1.65  
    1.66 -    rc
    1.67 +    find_sessions() foreach println
    1.68 +
    1.69 +    0
    1.70    }
    1.71  
    1.72  
    1.73 @@ -89,7 +95,7 @@
    1.74        Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    1.75          SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
    1.76  
    1.77 -    val session_info: Parser[Session_Info] =
    1.78 +    def session_info(dir: Path): Parser[Session_Info] =
    1.79      {
    1.80        val session_name = atom("session name", _.is_name)
    1.81        val theory_name = atom("theory name", _.is_name)
    1.82 @@ -113,14 +119,14 @@
    1.83          rep(theories) ~
    1.84          (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
    1.85            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    1.86 -            Session_Info(Path.current, a, b getOrElse a, c, d, e, f,
    1.87 +            Session_Info(dir, a, b getOrElse a, c, d, e, f,
    1.88                g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
    1.89      }
    1.90  
    1.91 -    def parse_entries(source: CharSequence): List[Session_Info] =
    1.92 +    def parse_entries(dir: Path, root: File): List[Session_Info] =
    1.93      {
    1.94 -      val in = Token.reader(syntax.scan(source))
    1.95 -      parse_all(rep(session_info), in) match {
    1.96 +      val toks = syntax.scan(Standard_System.read_file(root))
    1.97 +      parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
    1.98          case Success(result, _) => result
    1.99          case bad => error(bad.toString)
   1.100        }
   1.101 @@ -133,8 +139,8 @@
   1.102        dir <- Isabelle_System.components()
   1.103        root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
   1.104        if root.isFile
   1.105 -      entry <- Parser.parse_entries(Standard_System.read_file(root))
   1.106 -    } yield entry.copy(dir = dir)
   1.107 +      entry <- Parser.parse_entries(dir, root)
   1.108 +    } yield entry
   1.109    }
   1.110  }
   1.111