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