1.1 --- a/src/Pure/Isar/outer_parse.scala	Sat May 15 22:05:49 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,77 +0,0 @@
     1.4 -/*  Title:      Pure/Isar/outer_parse.scala
     1.5 -    Author:     Makarius
     1.6 -
     1.7 -Generic parsers for Isabelle/Isar outer syntax.
     1.8 -*/
     1.9 -
    1.10 -package isabelle
    1.11 -
    1.12 -import scala.util.parsing.combinator.Parsers
    1.13 -
    1.14 -
    1.15 -object Outer_Parse
    1.16 -{
    1.17 -  /* parsing tokens */
    1.18 -
    1.19 -  trait Parser extends Parsers
    1.20 -  {
    1.21 -    type Elem = Outer_Lex.Token
    1.22 -
    1.23 -    def filter_proper = true
    1.24 -
    1.25 -    private def proper(in: Input): Input =
    1.26 -      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
    1.27 -      else proper(in.rest)
    1.28 -
    1.29 -    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
    1.30 -    {
    1.31 -      def apply(raw_input: Input) =
    1.32 -      {
    1.33 -        val in = proper(raw_input)
    1.34 -        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
    1.35 -        else {
    1.36 -          val token = in.first
    1.37 -          if (pred(token)) Success(token, proper(in.rest))
    1.38 -          else
    1.39 -            token.text match {
    1.40 -              case (txt, "") =>
    1.41 -                Failure(s + " expected,\nbut " + txt + " was found", in)
    1.42 -              case (txt1, txt2) =>
    1.43 -                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
    1.44 -            }
    1.45 -        }
    1.46 -      }
    1.47 -    }
    1.48 -
    1.49 -    def not_eof: Parser[Elem] = token("input token", _ => true)
    1.50 -    def eof: Parser[Unit] = not(not_eof)
    1.51 -
    1.52 -    def atom(s: String, pred: Elem => Boolean): Parser[String] =
    1.53 -      token(s, pred) ^^ (_.content)
    1.54 -
    1.55 -    def keyword(name: String): Parser[String] =
    1.56 -      atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
    1.57 -        tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
    1.58 -
    1.59 -    def name: Parser[String] = atom("name declaration", _.is_name)
    1.60 -    def xname: Parser[String] = atom("name reference", _.is_xname)
    1.61 -    def text: Parser[String] = atom("text", _.is_text)
    1.62 -    def ML_source: Parser[String] = atom("ML source", _.is_text)
    1.63 -    def doc_source: Parser[String] = atom("document source", _.is_text)
    1.64 -    def path: Parser[String] = atom("file name/path specification", _.is_name)
    1.65 -
    1.66 -    private def tag_name: Parser[String] =
    1.67 -      atom("tag name", tok =>
    1.68 -          tok.kind == Outer_Lex.Token_Kind.IDENT ||
    1.69 -          tok.kind == Outer_Lex.Token_Kind.STRING)
    1.70 -
    1.71 -    def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
    1.72 -
    1.73 -
    1.74 -    /* wrappers */
    1.75 -
    1.76 -    def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
    1.77 -    def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
    1.78 -  }
    1.79 -}
    1.80 -

     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/parse.scala	Sat May 15 22:15:57 2010 +0200
     2.3 @@ -0,0 +1,77 @@
     2.4 +/*  Title:      Pure/Isar/outer_parse.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Generic parsers for Isabelle/Isar outer syntax.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +import scala.util.parsing.combinator.Parsers
    2.13 +
    2.14 +
    2.15 +object Parse
    2.16 +{
    2.17 +  /* parsing tokens */
    2.18 +
    2.19 +  trait Parser extends Parsers
    2.20 +  {
    2.21 +    type Elem = Outer_Lex.Token
    2.22 +
    2.23 +    def filter_proper = true
    2.24 +
    2.25 +    private def proper(in: Input): Input =
    2.26 +      if (in.atEnd || !in.first.is_ignored || !filter_proper) in
    2.27 +      else proper(in.rest)
    2.28 +
    2.29 +    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
    2.30 +    {
    2.31 +      def apply(raw_input: Input) =
    2.32 +      {
    2.33 +        val in = proper(raw_input)
    2.34 +        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
    2.35 +        else {
    2.36 +          val token = in.first
    2.37 +          if (pred(token)) Success(token, proper(in.rest))
    2.38 +          else
    2.39 +            token.text match {
    2.40 +              case (txt, "") =>
    2.41 +                Failure(s + " expected,\nbut " + txt + " was found", in)
    2.42 +              case (txt1, txt2) =>
    2.43 +                Failure(s + " expected,\nbut " + txt1 + " was found:\n" + txt2, in)
    2.44 +            }
    2.45 +        }
    2.46 +      }
    2.47 +    }
    2.48 +
    2.49 +    def not_eof: Parser[Elem] = token("input token", _ => true)
    2.50 +    def eof: Parser[Unit] = not(not_eof)
    2.51 +
    2.52 +    def atom(s: String, pred: Elem => Boolean): Parser[String] =
    2.53 +      token(s, pred) ^^ (_.content)
    2.54 +
    2.55 +    def keyword(name: String): Parser[String] =
    2.56 +      atom(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
    2.57 +        tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
    2.58 +
    2.59 +    def name: Parser[String] = atom("name declaration", _.is_name)
    2.60 +    def xname: Parser[String] = atom("name reference", _.is_xname)
    2.61 +    def text: Parser[String] = atom("text", _.is_text)
    2.62 +    def ML_source: Parser[String] = atom("ML source", _.is_text)
    2.63 +    def doc_source: Parser[String] = atom("document source", _.is_text)
    2.64 +    def path: Parser[String] = atom("file name/path specification", _.is_name)
    2.65 +
    2.66 +    private def tag_name: Parser[String] =
    2.67 +      atom("tag name", tok =>
    2.68 +          tok.kind == Outer_Lex.Token_Kind.IDENT ||
    2.69 +          tok.kind == Outer_Lex.Token_Kind.STRING)
    2.70 +
    2.71 +    def tags: Parser[List[String]] = rep(keyword("%") ~> tag_name)
    2.72 +
    2.73 +
    2.74 +    /* wrappers */
    2.75 +
    2.76 +    def parse[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = p(in)
    2.77 +    def parse_all[T](p: Parser[T], in: Outer_Lex.Reader): ParseResult[T] = parse(phrase(p), in)
    2.78 +  }
    2.79 +}
    2.80 +

     3.1 --- a/src/Pure/Thy/thy_header.scala	Sat May 15 22:05:49 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Sat May 15 22:15:57 2010 +0200
     3.3 @@ -27,7 +27,7 @@
     3.4  }
     3.5  
     3.6  
     3.7 -class Thy_Header(symbols: Symbol.Interpretation) extends Outer_Parse.Parser
     3.8 +class Thy_Header(symbols: Symbol.Interpretation) extends Parse.Parser
     3.9  {
    3.10    import Thy_Header._
    3.11  

     4.1 --- a/src/Pure/Thy/thy_syntax.scala	Sat May 15 22:05:49 2010 +0200
     4.2 +++ b/src/Pure/Thy/thy_syntax.scala	Sat May 15 22:15:57 2010 +0200
     4.3 @@ -9,7 +9,7 @@
     4.4  
     4.5  object Thy_Syntax
     4.6  {
     4.7 -  private val parser = new Outer_Parse.Parser
     4.8 +  private val parser = new Parse.Parser
     4.9    {
    4.10      override def filter_proper = false
    4.11  

     5.1 --- a/src/Pure/build-jars	Sat May 15 22:05:49 2010 +0200
     5.2 +++ b/src/Pure/build-jars	Sat May 15 22:15:57 2010 +0200
     5.3 @@ -35,8 +35,8 @@
     5.4    Isar/isar_document.scala
     5.5    Isar/keyword.scala
     5.6    Isar/outer_lex.scala
     5.7 -  Isar/outer_parse.scala
     5.8    Isar/outer_syntax.scala
     5.9 +  Isar/parse.scala
    5.10    PIDE/change.scala
    5.11    PIDE/command.scala
    5.12    PIDE/document.scala