# HG changeset patch
# User wenzelm
# Date 1261490443 -3600
# Node ID 903092d615192abb6b6fab31446ca169baa5a5f3
# Parent  8b66bd211dcfb34c547015fbb51a21f903406065
Generic parsers for Isabelle/Isar outer syntax -- Scala version.

diff -r 8b66bd211dcf -r 903092d61519 src/Pure/IsaMakefile
--- a/src/Pure/IsaMakefile	Tue Dec 22 15:00:03 2009 +0100
+++ b/src/Pure/IsaMakefile	Tue Dec 22 15:00:43 2009 +0100
@@ -125,11 +125,12 @@
   General/linear_set.scala General/markup.scala General/position.scala	\
   General/scan.scala General/swing_thread.scala General/symbol.scala	\
   General/xml.scala General/yxml.scala Isar/isar_document.scala		\
-  Isar/outer_keyword.scala Isar/outer_lex.scala System/cygwin.scala	\
-  System/gui_setup.scala System/isabelle_process.scala			\
-  System/isabelle_syntax.scala System/isabelle_system.scala		\
-  System/platform.scala Thy/completion.scala Thy/html.scala		\
-  Thy/thy_header.scala library.scala
+  Isar/outer_keyword.scala Isar/outer_lex.scala Isar/outer_parse.scala	\
+  System/cygwin.scala System/gui_setup.scala				\
+  System/isabelle_process.scala System/isabelle_syntax.scala		\
+  System/isabelle_system.scala System/platform.scala			\
+  Thy/completion.scala Thy/html.scala Thy/thy_header.scala		\
+  library.scala
 
 JAR_DIR = $(ISABELLE_HOME)/lib/classes
 PURE_JAR = $(JAR_DIR)/Pure.jar
diff -r 8b66bd211dcf -r 903092d61519 src/Pure/Isar/outer_parse.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Isar/outer_parse.scala	Tue Dec 22 15:00:43 2009 +0100
@@ -0,0 +1,52 @@
+/*  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
+{
+  trait Parser extends Parsers
+  {
+    type Elem = Outer_Lex.Token
+
+
+    /* basic parsers */
+
+    def token(s: String, pred: Elem => Boolean): Parser[Elem] = new Parser[Elem]
+    {
+      def apply(in: Input) =
+      {
+        if (in.atEnd) Failure(s + " expected (past end-of-file!)", in)
+        else {
+          val token = in.first
+          if (pred(token)) Success(token, 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 keyword(name: String): Parser[Elem] =
+      token(Outer_Lex.Token_Kind.KEYWORD.toString + " \"" + name + "\"",
+        tok => tok.kind == Outer_Lex.Token_Kind.KEYWORD && tok.content == name)
+
+    def name: Parser[Elem] = token("name declaration", _.is_name)
+    def xname: Parser[Elem] = token("name reference", _.is_xname)
+    def text: Parser[Elem] = token("text", _.is_text)
+    def path: Parser[Elem] = token("file name/path specification", _.is_name)
+  }
+}
+