/* Title: Pure/Isar/parse.scala Author: Makarius Generic parsers for Isabelle/Isar outer syntax. package isabelleimport scala.util.parsing.combinatorimport scala.annotation.tailrecobject Parse {/* parsing tokens */ trait Parsers extends combinator.Parsers {type Elem = Tokendef filter_proper: Boolean = true private def proper(in: Input): Input =if (!filter_proper || in.atEnd || in.first.is_proper) inelse proper(in.rest)private def proper_position: Parser[Position.T] =new Parser[Position.T] {def apply(raw_input: Input) = {val in = proper(raw_input)val pos =match {case pos: Token.Pos => poscase _ => Token.Pos.noneif (in.atEnd) pos.position() else pos.position(in.first), in)def position[A](parser: Parser[A]): Parser[(A, Position.T)] =case x ~ y => (y, x) }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.firstif (pred(token)) Success(token, proper(in.rest))else Failure(s + " expected,\nbut " + token.kind + " was found:\n" + token.source, in)def atom(s: String, pred: Elem => Boolean): Parser[String] =def command(name: String): Parser[String] = atom("command " + quote(name), _.is_command(name))def $$$(name: String): Parser[String] = atom("keyword " + quote(name), _.is_keyword(name))def string: Parser[String] = atom("string" , _.is_string)def nat: Parser[Int] = atom("natural number" , _.is_nat) ^^ (s => Integer.parseInt(s))def name: Parser[String] = atom("name" , _.is_name)def embedded: Parser[String] = atom("embedded content" , _.is_embedded)def text: Parser[String] = atom("text" , _.is_embedded)def ML_source: Parser[String] = atom("ML source" , _.is_embedded)def document_source: Parser[String] = atom("document source" , _.is_embedded)def opt_keyword(s: String): Parser[Boolean] ="(" ) ~! $$$(s) ~ $$$(")" )) ^^ (_ => true ) | success(false )def path: Parser[String] ="file name/path specification" , tok => tok.is_embedded && Path.is_wellformed(tok.content))def in_path(default: String): Parser[String] ="in" ) ~! path ^^ { case _ ~ x => x } | success(default)def in_path_parens(default: String): Parser[String] ="(" ) ~! ($$$("in" ) ~ path ~ $$$(")" )) ^^ { case _ ~ (_ ~ x ~ _) => x } | success(default)def chapter_name: Parser[String] = atom("chapter name" , _.is_system_name)def session_name: Parser[String] = atom("session name" , _.is_system_name)def theory_name: Parser[String] = atom("theory name" , _.is_system_name)private def tag_name: Parser[String] ="tag name" , tok =>def tag: Parser[String] = $$$("%" ) ~> tag_namedef tags: Parser[List[String]] = rep(tag)def marker: Parser[String] = token("marker" , _.is_marker) ^^ (_.content)def annotation: Parser[Unit] = rep(tag | marker) ^^ (_ => ())/* wrappers */ def parse[T](p: Parser[T], in: Token.Reader): ParseResult[T] = p(in)def parse_all[T](p: Parser[T], in: Token.Reader): ParseResult[T] = {val result = parse(p, in)val rest = proper(result.next)if (result.successful && !rest.atEnd) Error("bad input" , rest)else resultquality 100%
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
