# HG changeset patch # User wenzelm # Date 1396956248 -7200 # Node ID 555f4be59be646ab144f378c7689a95491e72371 # Parent 013dfac0811a7527259e10746d6c8cabb1807a91 more precise token positions; diff -r 013dfac0811a -r 555f4be59be6 src/Pure/General/position.scala --- a/src/Pure/General/position.scala Tue Apr 08 12:31:17 2014 +0200 +++ b/src/Pure/General/position.scala Tue Apr 08 13:24:08 2014 +0200 @@ -30,6 +30,10 @@ object Line_File { + def apply(line: Int, file: String): T = + (if (line > 0) Line(line) else Nil) ::: + (if (file != "") File(file) else Nil) + def unapply(pos: T): Option[(Int, String)] = (pos, pos) match { case (Line(i), File(name)) => Some((i, name)) diff -r 013dfac0811a -r 555f4be59be6 src/Pure/Isar/parse.scala --- a/src/Pure/Isar/parse.scala Tue Apr 08 12:31:17 2014 +0200 +++ b/src/Pure/Isar/parse.scala Tue Apr 08 13:24:08 2014 +0200 @@ -25,31 +25,37 @@ if (!filter_proper || in.atEnd || in.first.is_proper) in else proper(in.rest) - def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem] - { - def apply(raw_input: Input) = - { - val in = proper(raw_input) - if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) - else { - val token = in.first - if (pred(token)) Success(token, proper(in.rest)) - else - token.text match { - case (txt, "") => - Failure(s + " expected,\nbut " + txt + " was found", in) - case (txt1, txt2) => - Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in) - } + def token(s: String, pred: Elem => Boolean): Parser[(Elem, Token.Pos)] = + new Parser[(Elem, Token.Pos)] { + def apply(raw_input: Input) = + { + val in = proper(raw_input) + if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) + else { + val pos = + in.pos match { + case pos: Token.Pos => pos + case _ => Token.Pos.none + } + val token = in.first + if (pred(token)) Success((token, pos), proper(in.rest)) + else + token.text match { + case (txt, "") => + Failure(s + " expected,\nbut " + txt + " was found", in) + case (txt1, txt2) => + Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in) + } + } } } - } def atom(s: String, pred: Elem => Boolean): Parser[String] = - token(s, pred) ^^ (_.content) + token(s, pred) ^^ { case (tok, _) => tok.content } - def command(name: String): Parser[String] = - atom("command " + quote(name), tok => tok.is_command && tok.source == name) + def command(name: String): Parser[Position.T] = + token("command " + quote(name), tok => tok.is_command && tok.source == name) ^^ + { case (_, pos) => pos.position } def keyword(name: String): Parser[String] = atom("keyword " + quote(name), tok => tok.is_keyword && tok.source == name) diff -r 013dfac0811a -r 555f4be59be6 src/Pure/Isar/token.scala --- a/src/Pure/Isar/token.scala Tue Apr 08 12:31:17 2014 +0200 +++ b/src/Pure/Isar/token.scala Tue Apr 08 13:24:08 2014 +0200 @@ -121,25 +121,31 @@ /* token reader */ - class Position(val line: Int, val file: String) extends scala.util.parsing.input.Position + object Pos + { + val none: Pos = new Pos(0, "") + } + + final class Pos private[Token](val line: Int, val file: String) + extends scala.util.parsing.input.Position { def column = 0 def lineContents = "" - override def toString = - if (file == "") ("line " + line.toString) - else ("line " + line.toString + " of " + quote(file)) - def advance(token: Token): Position = + def advance(token: Token): Pos = { var n = 0 for (c <- token.content if c == '\n') n += 1 - if (n == 0) this else new Position(line + n, file) + if (n == 0) this else new Pos(line + n, file) } + + def position: Position.T = Position.Line_File(line, file) + override def toString: String = Position.here(position) } abstract class Reader extends scala.util.parsing.input.Reader[Token] - private class Token_Reader(tokens: List[Token], val pos: Position) extends Reader + private class Token_Reader(tokens: List[Token], val pos: Pos) extends Reader { def first = tokens.head def rest = new Token_Reader(tokens.tail, pos.advance(first)) @@ -147,7 +153,7 @@ } def reader(tokens: List[Token], file: String = ""): Reader = - new Token_Reader(tokens, new Position(1, file)) + new Token_Reader(tokens, new Pos(1, file)) } diff -r 013dfac0811a -r 555f4be59be6 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Tue Apr 08 12:31:17 2014 +0200 +++ b/src/Pure/Tools/build.scala Tue Apr 08 13:24:08 2014 +0200 @@ -203,16 +203,14 @@ private object Parser extends Parse.Parser { - def entry(pos: Position.T): Parser[Entry] = chapter(pos) | session_entry(pos) - - def chapter(pos: Position.T): Parser[Chapter] = + val chapter: Parser[Chapter] = { val chapter_name = atom("chapter name", _.is_name) command(CHAPTER) ~! chapter_name ^^ { case _ ~ a => Chapter(a) } } - def session_entry(pos: Position.T): Parser[Session_Entry] = + val session_entry: Parser[Session_Entry] = { val session_name = atom("session name", _.is_name) @@ -234,7 +232,7 @@ ((keyword(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~ rep1(theories) ~ ((keyword(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil))))) ^^ - { case _ ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) => + { case pos ~ (a ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h))) => Session_Entry(pos, a, b, c, d, e, f, g, h) } } @@ -242,7 +240,7 @@ { val toks = root_syntax.scan(File.read(root)) - parse_all(rep(entry(root.position)), Token.reader(toks, root.implode)) match { + parse_all(rep(chapter | session_entry), Token.reader(toks, root.implode)) match { case Success(result, _) => var chapter = chapter_default val entries = new mutable.ListBuffer[(String, Session_Entry)]