Efficient scanning of literals.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/scan.scala	Tue Jun 16 15:25:32 2009 +0200
@@ -0,0 +1,82 @@
+/*  Title:      Pure/General/scan.scala
+    Author:     Makarius
+
+Efficient scanning of literals.
+*/
+
+package isabelle
+
+import scala.util.parsing.combinator.RegexParsers
+
+
+object Scan
+{
+
+  /* class Lexicon -- position tree */
+
+  case class Lexicon(val tab: Map[Char, (Boolean, Lexicon)])
+
+  val empty_lexicon = Lexicon(Map())
+
+  def is_literal(lx: Lexicon, str: CharSequence): Boolean =
+  {
+    val len = str.length
+    def is_lit(lexicon: Lexicon, i: Int): Boolean =
+      i < len && {
+        lexicon.tab.get(str.charAt(i)) match {
+          case Some((tip, lex)) => tip && i + 1 == len || is_lit(lex, i + 1)
+          case None => false
+        }
+      }
+    is_lit(lx, 0)
+  }
+
+  def extend_lexicon(lx: Lexicon, str: CharSequence): Lexicon =
+  {
+    val len = str.length
+    def ext(lexicon: Lexicon, i: Int): Lexicon =
+      if (i == len) lexicon
+      else {
+        val c = str.charAt(i)
+        val is_last = (i + 1 == len)
+        lexicon.tab.get(c) match {
+          case Some((tip, lex)) => Lexicon(lexicon.tab + (c -> (tip || is_last, ext(lex, i + 1))))
+          case None => Lexicon(lexicon.tab + (c -> (is_last, ext(empty_lexicon, i + 1))))
+        }
+      }
+    if (is_literal(lx, str)) lx else ext(lx, 0)
+  }
+
+}
+
+
+class Scan extends RegexParsers
+{
+  override val whiteSpace = "".r
+
+  def keyword(lx: Scan.Lexicon): Parser[String] = new Parser[String] {
+    def apply(in: Input) =
+    {
+      val source = in.source
+      val offset = in.offset
+      val len = source.length - offset
+
+      def scan(lexicon: Scan.Lexicon, i: Int, res: Int): Int =
+      {
+        if (i < len) {
+          lexicon.tab.get(source.charAt(offset + i)) match {
+            case Some((tip, lex)) => scan(lex, i + 1, if (tip) i + 1 else res)
+            case None => res
+          }
+        } else res
+      }
+      scan(lx, 0, 0) match {
+        case res if res > 0 =>
+          Success(source.subSequence(offset, res).toString, in.drop(res))
+        case _ => Failure("keyword expected", in)
+      }
+    }
+  }.named("keyword")
+
+}
+

--- a/src/Pure/IsaMakefile	Mon Jun 15 21:33:27 2009 +0200
+++ b/src/Pure/IsaMakefile	Tue Jun 16 15:25:32 2009 +0200
@@ -115,9 +115,9 @@
 ## Scala material
 
 SCALA_FILES = General/event_bus.scala General/markup.scala		\
-  General/position.scala General/swing.scala General/symbol.scala	\
-  General/xml.scala General/yxml.scala Isar/isar.scala			\
-  Isar/isar_document.scala Isar/outer_keyword.scala			\
+  General/position.scala General/scan.scala General/swing.scala		\
+  General/symbol.scala General/xml.scala General/yxml.scala		\
+  Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
   System/cygwin.scala System/isabelle_process.scala			\
   System/isabelle_system.scala Thy/thy_header.scala			\
   Tools/isabelle_syntax.scala