1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/scan.scala	Tue Jun 16 15:25:32 2009 +0200
     1.3 @@ -0,0 +1,82 @@
     1.4 +/*  Title:      Pure/General/scan.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Efficient scanning of literals.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +import scala.util.parsing.combinator.RegexParsers
    1.13 +
    1.14 +
    1.15 +object Scan
    1.16 +{
    1.17 +
    1.18 +  /* class Lexicon -- position tree */
    1.19 +
    1.20 +  case class Lexicon(val tab: Map[Char, (Boolean, Lexicon)])
    1.21 +
    1.22 +  val empty_lexicon = Lexicon(Map())
    1.23 +
    1.24 +  def is_literal(lx: Lexicon, str: CharSequence): Boolean =
    1.25 +  {
    1.26 +    val len = str.length
    1.27 +    def is_lit(lexicon: Lexicon, i: Int): Boolean =
    1.28 +      i < len && {
    1.29 +        lexicon.tab.get(str.charAt(i)) match {
    1.30 +          case Some((tip, lex)) => tip && i + 1 == len || is_lit(lex, i + 1)
    1.31 +          case None => false
    1.32 +        }
    1.33 +      }
    1.34 +    is_lit(lx, 0)
    1.35 +  }
    1.36 +
    1.37 +  def extend_lexicon(lx: Lexicon, str: CharSequence): Lexicon =
    1.38 +  {
    1.39 +    val len = str.length
    1.40 +    def ext(lexicon: Lexicon, i: Int): Lexicon =
    1.41 +      if (i == len) lexicon
    1.42 +      else {
    1.43 +        val c = str.charAt(i)
    1.44 +        val is_last = (i + 1 == len)
    1.45 +        lexicon.tab.get(c) match {
    1.46 +          case Some((tip, lex)) => Lexicon(lexicon.tab + (c -> (tip || is_last, ext(lex, i + 1))))
    1.47 +          case None => Lexicon(lexicon.tab + (c -> (is_last, ext(empty_lexicon, i + 1))))
    1.48 +        }
    1.49 +      }
    1.50 +    if (is_literal(lx, str)) lx else ext(lx, 0)
    1.51 +  }
    1.52 +
    1.53 +}
    1.54 +
    1.55 +
    1.56 +class Scan extends RegexParsers
    1.57 +{
    1.58 +  override val whiteSpace = "".r
    1.59 +
    1.60 +  def keyword(lx: Scan.Lexicon): Parser[String] = new Parser[String] {
    1.61 +    def apply(in: Input) =
    1.62 +    {
    1.63 +      val source = in.source
    1.64 +      val offset = in.offset
    1.65 +      val len = source.length - offset
    1.66 +
    1.67 +      def scan(lexicon: Scan.Lexicon, i: Int, res: Int): Int =
    1.68 +      {
    1.69 +        if (i < len) {
    1.70 +          lexicon.tab.get(source.charAt(offset + i)) match {
    1.71 +            case Some((tip, lex)) => scan(lex, i + 1, if (tip) i + 1 else res)
    1.72 +            case None => res
    1.73 +          }
    1.74 +        } else res
    1.75 +      }
    1.76 +      scan(lx, 0, 0) match {
    1.77 +        case res if res > 0 =>
    1.78 +          Success(source.subSequence(offset, res).toString, in.drop(res))
    1.79 +        case _ => Failure("keyword expected", in)
    1.80 +      }
    1.81 +    }
    1.82 +  }.named("keyword")
    1.83 +
    1.84 +}
    1.85 +

     2.1 --- a/src/Pure/IsaMakefile	Mon Jun 15 21:33:27 2009 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Tue Jun 16 15:25:32 2009 +0200
     2.3 @@ -115,9 +115,9 @@
     2.4  ## Scala material
     2.5  
     2.6  SCALA_FILES = General/event_bus.scala General/markup.scala		\
     2.7 -  General/position.scala General/swing.scala General/symbol.scala	\
     2.8 -  General/xml.scala General/yxml.scala Isar/isar.scala			\
     2.9 -  Isar/isar_document.scala Isar/outer_keyword.scala			\
    2.10 +  General/position.scala General/scan.scala General/swing.scala		\
    2.11 +  General/symbol.scala General/xml.scala General/yxml.scala		\
    2.12 +  Isar/isar.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
    2.13    System/cygwin.scala System/isabelle_process.scala			\
    2.14    System/isabelle_system.scala Thy/thy_header.scala			\
    2.15    Tools/isabelle_syntax.scala