--- a/src/Pure/Isar/outer_parse.scala Sat May 15 22:05:49 2010 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,77 +0,0 @@
-/* Title: Pure/Isar/outer_parse.scala
- Author: Makarius
-
-Generic parsers for Isabelle/Isar outer syntax.
-*/
-
-package isabelle
-
-import scala.util.parsing.combinator.Parsers
-
-
-object Outer_Parse
-{
- /* parsing tokens */
-
- trait Parser extends Parsers
- {
- type Elem = Outer_Lex.Token
-
- def filter_proper = true
-
- private def proper(in: Input): Input =
- if (in.atEnd || !in.first.is_ignored || !filter_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 (past end-of-file!)", 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 not_eof: Parser[Elem] = token("input token", _ => true)
- def eof: Parser[Unit] = not(not_eof)
-
- def atom(s: String, pred: Elem => Boolean): Parser[String] =
- token(s, pred) ^^ (_.content)
-
- def keyword(name: String): Parser[String] =
- atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
- tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
-
- def name: Parser[String] = atom("name declaration", _.is_name)
- def xname: Parser[String] = atom("name reference", _.is_xname)
- def text: Parser[String] = atom("text", _.is_text)
- def ML_source: Parser[String] = atom("ML source", _.is_text)
- def doc_source: Parser[String] = atom("document source", _.is_text)
- def path: Parser[String] = atom("file name/path specification", _.is_name)
-
- private def tag_name: Parser[String] =
- atom("tag name", tok =>
- tok.kind == Outer_Lex.Token_Kind.IDENT ||
- tok.kind == Outer_Lex.Token_Kind.STRING)
-
- def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
-
-
- /* wrappers */
-
- def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
- def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
- }
-}
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/parse.scala Sat May 15 22:15:57 2010 +0200
@@ -0,0 +1,77 @@
+/* Title: Pure/Isar/outer_parse.scala
+ Author: Makarius
+
+Generic parsers for Isabelle/Isar outer syntax.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.Parsers
+
+
+object Parse
+{
+ /* parsing tokens */
+
+ trait Parser extends Parsers
+ {
+ type Elem = Outer_Lex.Token
+
+ def filter_proper = true
+
+ private def proper(in: Input): Input =
+ if (in.atEnd || !in.first.is_ignored || !filter_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 (past end-of-file!)", 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 not_eof: Parser[Elem] = token("input token", _ => true)
+ def eof: Parser[Unit] = not(not_eof)
+
+ def atom(s: String, pred: Elem => Boolean): Parser[String] =
+ token(s, pred) ^^ (_.content)
+
+ def keyword(name: String): Parser[String] =
+ atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
+ tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
+
+ def name: Parser[String] = atom("name declaration", _.is_name)
+ def xname: Parser[String] = atom("name reference", _.is_xname)
+ def text: Parser[String] = atom("text", _.is_text)
+ def ML_source: Parser[String] = atom("ML source", _.is_text)
+ def doc_source: Parser[String] = atom("document source", _.is_text)
+ def path: Parser[String] = atom("file name/path specification", _.is_name)
+
+ private def tag_name: Parser[String] =
+ atom("tag name", tok =>
+ tok.kind == Outer_Lex.Token_Kind.IDENT ||
+ tok.kind == Outer_Lex.Token_Kind.STRING)
+
+ def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
+
+
+ /* wrappers */
+
+ def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
+ def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
+ }
+}
+
--- a/src/Pure/Thy/thy_header.scala Sat May 15 22:05:49 2010 +0200
+++ b/src/Pure/Thy/thy_header.scala Sat May 15 22:15:57 2010 +0200
@@ -27,7 +27,7 @@
}
-class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser
+class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser
{
import Thy_Header._
--- a/src/Pure/Thy/thy_syntax.scala Sat May 15 22:05:49 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Sat May 15 22:15:57 2010 +0200
@@ -9,7 +9,7 @@
object Thy_Syntax
{
- private val parser = new Outer_Parse.Parser
+ private val parser = new Parse.Parser
{
override def filter_proper = false
--- a/src/Pure/build-jars Sat May 15 22:05:49 2010 +0200
+++ b/src/Pure/build-jars Sat May 15 22:15:57 2010 +0200
@@ -35,8 +35,8 @@
Isar/isar_document.scala
Isar/keyword.scala
Isar/outer_lex.scala
- Isar/outer_parse.scala
Isar/outer_syntax.scala
+ Isar/parse.scala
PIDE/change.scala
PIDE/command.scala
PIDE/document.scala