1/* Title: Pure/Isar/parse.scala 2 Author: Makarius 3 4Generic parsers for Isabelle/Isar outer syntax. 5*/ 6 7package isabelle 8 9 10import scala.util.parsing.combinator.Parsers 11import scala.annotation.tailrec 12 13 14object Parse 15{ 16 /* parsing tokens */ 17 18 trait Parser extends Parsers 19 { 20 type Elem = Token 21 22 def filter_proper: Boolean = true 23 24 @tailrec private def proper(in: Input): Input = 25 if (!filter_proper || in.atEnd || in.first.is_proper) in 26 else proper(in.rest) 27 28 private def proper_position: Parser[Position.T] = 29 new Parser[Position.T] { 30 def apply(raw_input: Input) = 31 { 32 val in = proper(raw_input) 33 val pos = 34 in.pos match { 35 case pos: Token.Pos => pos 36 case _ => Token.Pos.none 37 } 38 Success(if (in.atEnd) pos.position() else pos.position(in.first), in) 39 } 40 } 41 42 def position[A](parser: Parser[A]): Parser[(A, Position.T)] = 43 proper_position ~ parser ^^ { case x ~ y => (y, x) } 44 45 def token(s: String, pred: Elem => Boolean): Parser[Elem] = 46 new Parser[Elem] { 47 def apply(raw_input: Input) = 48 { 49 val in = proper(raw_input) 50 if (in.atEnd) Failure(s + " expected,\nbut end-of-input was found", in) 51 else { 52 val token = in.first 53 if (pred(token)) Success(token, proper(in.rest)) 54 else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in) 55 } 56 } 57 } 58 59 def atom(s: String, pred: Elem => Boolean): Parser[String] = 60 token(s, pred) ^^ (_.content) 61 62 def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name)) 63 def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name)) 64 def string: Parser[String] = atom("string", _.is_string) 65 def nat: Parser[Int] = atom("natural number", _.is_nat) ^^ (s => Integer.parseInt(s)) 66 def name: Parser[String] = atom("name", _.is_name) 67 def embedded: Parser[String] = atom("embedded content", _.is_embedded) 68 def text: Parser[String] = atom("text", _.is_text) 69 def ML_source: Parser[String] = atom("ML source", _.is_text) 70 def document_source: Parser[String] = atom("document source", _.is_text) 71 72 def path: Parser[String] = 73 atom("file name/path specification", tok => tok.is_embedded && Path.is_wellformed(tok.content)) 74 75 def session_name: Parser[String] = atom("session name", _.is_system_name) 76 def theory_name: Parser[String] = atom("theory name", _.is_system_name) 77 78 private def tag_name: Parser[String] = 79 atom("tag name", tok => 80 tok.kind == Token.Kind.IDENT || 81 tok.kind == Token.Kind.STRING) 82 83 def tags: Parser[List[String]] = rep($$$("%") ~> tag_name) 84 85 86 /* wrappers */ 87 88 def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in) 89 90 def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = 91 { 92 val result = parse(p, in) 93 val rest = proper(result.next) 94 if (result.successful && !rest.atEnd) Error("bad input", rest) 95 else result 96 } 97 } 98} 99 100