# HG changeset patch
# User wenzelm
# Date 1342613251 -7200
# Node ID 2f923e99405666f1e2715aa229bdc458dacfb556
# Parent  8dff9933e72a9d9f0a954e6fcc50991bc04343c1
more informative errors;

diff -r 8dff9933e72a -r 2f923e994056 src/Pure/Isar/token.scala
--- a/src/Pure/Isar/token.scala	Wed Jul 18 13:43:36 2012 +0200
+++ b/src/Pure/Isar/token.scala	Wed Jul 18 14:07:31 2012 +0200
@@ -34,30 +34,33 @@
 
   /* token reader */
 
-  class Line_Position(val line: Int) extends scala.util.parsing.input.Position
+  class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position
   {
     def column = 0
     def lineContents = ""
-    override def toString = line.toString
+    override def toString =
+      if (file == "") ("line " + line.toString)
+      else ("line " + line.toString + " of " + quote(file))
 
-    def advance(token: Token): Line_Position =
+    def advance(token: Token): Position =
     {
       var n = 0
       for (c <- token.content if c == '\n') n += 1
-      if (n == 0) this else new Line_Position(line + n)
+      if (n == 0) this else new Position(line + n, file)
     }
   }
 
   abstract class Reader extends scala.util.parsing.input.Reader[Token]
 
-  private class Token_Reader(tokens: List[Token], val pos: Line_Position) extends Reader
+  private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader
   {
     def first = tokens.head
     def rest = new Token_Reader(tokens.tail, pos.advance(first))
     def atEnd = tokens.isEmpty
   }
 
-  def reader(tokens: List[Token]): Reader = new Token_Reader(tokens, new Line_Position(1))
+  def reader(tokens: List[Token], file: String = ""): Reader =
+    new Token_Reader(tokens, new Position(1, file))
 }
 
 
diff -r 8dff9933e72a -r 2f923e994056 src/Pure/System/build.scala
--- a/src/Pure/System/build.scala	Wed Jul 18 13:43:36 2012 +0200
+++ b/src/Pure/System/build.scala	Wed Jul 18 14:07:31 2012 +0200
@@ -7,6 +7,9 @@
 package isabelle
 
 
+import java.io.File
+
+
 object Build
 {
   /* command line entry point */
@@ -23,24 +26,27 @@
 
   def main(args: Array[String])
   {
-    def bad_args()
-    {
-      java.lang.System.err.println("Bad arguments: " + args.toString)
-      sys.exit(2)
-    }
+    def bad_args(): Nothing = error("Bad arguments: " + args.toString)
 
-    args.toList match {
-      case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
-        rest.indexWhere(_ == "\n") match {
-          case -1 => bad_args()
-          case i =>
-            val (options, rest1) = rest.splitAt(i)
-            val sessions = rest1.tail
-            val rc = build(all_sessions, build_images, list_only, options, sessions)
-            sys.exit(rc)
+    val rc =
+      try {
+        args.toList match {
+          case Bool(all_sessions) :: Bool(build_images) :: Bool(list_only) :: rest =>
+            rest.indexWhere(_ == "\n") match {
+              case -1 => bad_args()
+              case i =>
+                val (options, rest1) = rest.splitAt(i)
+                val sessions = rest1.tail
+                build(all_sessions, build_images, list_only, options, sessions)
+            }
+          case _ => bad_args()
         }
-      case _ => bad_args()
-    }
+      }
+      catch {
+        case exn: Throwable => java.lang.System.err.println(Exn.message(exn)); 2
+      }
+
+    sys.exit(rc)
   }
 
 
@@ -49,12 +55,12 @@
   def build(all_sessions: Boolean, build_images: Boolean, list_only: Boolean,
     options: List[String], sessions: List[String]): Int =
   {
-    val rc = 1
-
     println("options = " + options.toString)
     println("sessions = " + sessions.toString)
 
-    rc
+    find_sessions() foreach println
+
+    0
   }
 
 
@@ -89,7 +95,7 @@
       Outer_Syntax.empty + "(" + ")" + "+" + "," + "=" + "[" + "]" +
         SESSION + IN + NAME + DESCRIPTION + OPTIONS + THEORIES + FILES
 
-    val session_info: Parser[Session_Info] =
+    def session_info(dir: Path): Parser[Session_Info] =
     {
       val session_name = atom("session name", _.is_name)
       val theory_name = atom("theory name", _.is_name)
@@ -113,14 +119,14 @@
         rep(theories) ~
         (keyword(FILES) ~! rep1(file_name) ^^ { case _ ~ x => x } | success(Nil)) ^^
           { case a ~ b ~ c ~ d ~ e ~ f ~ g ~ h =>
-            Session_Info(Path.current, a, b getOrElse a, c, d, e, f,
+            Session_Info(dir, a, b getOrElse a, c, d, e, f,
               g.map({ case (x, ys) => ys.map(y => (x, y)) }).flatten, h) }
     }
 
-    def parse_entries(source: CharSequence): List[Session_Info] =
+    def parse_entries(dir: Path, root: File): List[Session_Info] =
     {
-      val in = Token.reader(syntax.scan(source))
-      parse_all(rep(session_info), in) match {
+      val toks = syntax.scan(Standard_System.read_file(root))
+      parse_all(rep(session_info(dir)), Token.reader(toks, root.toString)) match {
         case Success(result, _) => result
         case bad => error(bad.toString)
       }
@@ -133,8 +139,8 @@
       dir <- Isabelle_System.components()
       root = Isabelle_System.platform_file(dir + Path.basic(ROOT_NAME))
       if root.isFile
-      entry <- Parser.parse_entries(Standard_System.read_file(root))
-    } yield entry.copy(dir = dir)
+      entry <- Parser.parse_entries(dir, root)
+    } yield entry
   }
 }