# HG changeset patch
# User wenzelm
# Date 1273954557 -7200
# Node ID d2cdad45fd1489addb4c6a6e540f560861aa46f1
# Parent  285b39022372ab2aacdf8ef1204def204b2bf030
renamed Outer_Parse to Parse (in Scala);

diff -r 285b39022372 -r d2cdad45fd14 src/Pure/Isar/outer_parse.scala
--- 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)
-  }
-}
-
diff -r 285b39022372 -r d2cdad45fd14 src/Pure/Isar/parse.scala
--- /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)
+  }
+}
+
diff -r 285b39022372 -r d2cdad45fd14 src/Pure/Thy/thy_header.scala
--- 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._
 
diff -r 285b39022372 -r d2cdad45fd14 src/Pure/Thy/thy_syntax.scala
--- 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
 
diff -r 285b39022372 -r d2cdad45fd14 src/Pure/build-jars
--- 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