more informative errors;
authorwenzelm
Wed Jul 18 14:07:31 2012 +0200 (2012-07-18)
changeset 483352f923e994056
parent 48334 8dff9933e72a
child 48336 3c55bfad22eb
more informative errors;
src/Pure/Isar/token.scala
src/Pure/System/build.scala
     1.1 --- a/src/Pure/Isar/token.scala	Wed Jul 18 13:43:36 2012 +0200
     1.2 +++ b/src/Pure/Isar/token.scala	Wed Jul 18 14:07:31 2012 +0200
     1.3 @@ -34,30 +34,33 @@
     1.4  
     1.5    /* token reader */
     1.6  
     1.7 -  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
     1.8 +  class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position
     1.9    {
    1.10      def column = 0
    1.11      def lineContents = ""
    1.12 -    override def toString = line.toString
    1.13 +    override def toString =
    1.14 +      if (file == "") ("line " + line.toString)
    1.15 +      else ("line " + line.toString + " of " + quote(file))
    1.16  
    1.17 -    def advance(token: Token): Line_Position =
    1.18 +    def advance(token: Token): Position =
    1.19      {
    1.20        var n = 0
    1.21        for (c <- token.content if c == '\n') n += 1
    1.22 -      if (n == 0) this else new Line_Position(line + n)
    1.23 +      if (n == 0) this else new Position(line + n, file)
    1.24      }
    1.25    }
    1.26  
    1.27    abstract class Reader extends scala.util.parsing.input.Reader[Token]
    1.28  
    1.29 -  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
    1.30 +  private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader
    1.31    {
    1.32      def first = tokens.head
    1.33      def rest = new Token_Reader(tokens.tail, pos.advance(first))
    1.34      def atEnd = tokens.isEmpty
    1.35    }
    1.36  
    1.37 -  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
    1.38 +  def reader(tokens: List[Token], file: String = ""): Reader =
    1.39 +    new Token_Reader(tokens, new Position(1, file))
    1.40  }
    1.41  
    1.42  
     2.1 --- a/src/Pure/System/build.scala	Wed Jul 18 13:43:36 2012 +0200
     2.2 +++ b/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
     2.3 @@ -7,6 +7,9 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.io.File
     2.8 +
     2.9 +
    2.10  object Build
    2.11  {
    2.12    /* command line entry point */
    2.13 @@ -23,24 +26,27 @@
    2.14  
    2.15    def main(args: Array[String])
    2.16    {
    2.17 -    def bad_args()
    2.18 -    {
    2.19 -      java.lang.System.err.println("Bad arguments: " + args.toString)
    2.20 -      sys.exit(2)
    2.21 -    }
    2.22 +    def bad_args(): Nothing = error("Bad arguments: " + args.toString)
    2.23  
    2.24 -    args.toList match {
    2.25 -      case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
    2.26 -        rest.indexWhere(_ == "\n") match {
    2.27 -          case -1 => bad_args()
    2.28 -          case i =>
    2.29 -            val (options, rest1) = rest.splitAt(i)
    2.30 -            val sessions = rest1.tail
    2.31 -            val rc = build(all_sessions, build_images, list_only, options, sessions)
    2.32 -            sys.exit(rc)
    2.33 +    val rc =
    2.34 +      try {
    2.35 +        args.toList match {
    2.36 +          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
    2.37 +            rest.indexWhere(_ == "\n") match {
    2.38 +              case -1 => bad_args()
    2.39 +              case i =>
    2.40 +                val (options, rest1) = rest.splitAt(i)
    2.41 +                val sessions = rest1.tail
    2.42 +                build(all_sessions, build_images, list_only, options, sessions)
    2.43 +            }
    2.44 +          case _ => bad_args()
    2.45          }
    2.46 -      case _ => bad_args()
    2.47 -    }
    2.48 +      }
    2.49 +      catch {
    2.50 +        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
    2.51 +      }
    2.52 +
    2.53 +    sys.exit(rc)
    2.54    }
    2.55  
    2.56  
    2.57 @@ -49,12 +55,12 @@
    2.58    def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
    2.59      options: List[String], sessions: List[String]): Int =
    2.60    {
    2.61 -    val rc = 1
    2.62 -
    2.63      println("options = " + options.toString)
    2.64      println("sessions = " + sessions.toString)
    2.65  
    2.66 -    rc
    2.67 +    find_sessions() foreach println
    2.68 +
    2.69 +    0
    2.70    }
    2.71  
    2.72  
    2.73 @@ -89,7 +95,7 @@
    2.74        Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
    2.75          SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
    2.76  
    2.77 -    val session_info: Parser[Session_Info] =
    2.78 +    def session_info(dir: Path): Parser[Session_Info] =
    2.79      {
    2.80        val session_name = atom("session name", _.is_name)
    2.81        val theory_name = atom("theory name", _.is_name)
    2.82 @@ -113,14 +119,14 @@
    2.83          rep(theories) ~
    2.84          (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
    2.85            { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
    2.86 -            Session_Info(Path.current, a, b getOrElse a, c, d, e, f,
    2.87 +            Session_Info(dir, a, b getOrElse a, c, d, e, f,
    2.88                g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
    2.89      }
    2.90  
    2.91 -    def parse_entries(source: CharSequence): List[Session_Info] =
    2.92 +    def parse_entries(dir: Path, root: File): List[Session_Info] =
    2.93      {
    2.94 -      val in = Token.reader(syntax.scan(source))
    2.95 -      parse_all(rep(session_info), in) match {
    2.96 +      val toks = syntax.scan(Standard_System.read_file(root))
    2.97 +      parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
    2.98          case Success(result, _) => result
    2.99          case bad => error(bad.toString)
   2.100        }
   2.101 @@ -133,8 +139,8 @@
   2.102        dir <- Isabelle_System.components()
   2.103        root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
   2.104        if root.isFile
   2.105 -      entry <- Parser.parse_entries(Standard_System.read_file(root))
   2.106 -    } yield entry.copy(dir = dir)
   2.107 +      entry <- Parser.parse_entries(dir, root)
   2.108 +    } yield entry
   2.109    }
   2.110  }
   2.111