src/Pure/Isar/outer_syntax.scala
changeset 34166 446a33b874b3
child 34264 b5025782a4ed
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 22 19:38:06 2009 +0100
     1.3 @@ -0,0 +1,54 @@
     1.4 +/*  Title:      Pure/Isar/outer_syntax.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Isabelle/Isar outer syntax.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +import scala.util.parsing.input.{Reader, CharSequenceReader}
    1.14 +
    1.15 +
    1.16 +class Outer_Syntax(symbols: Symbol.Interpretation)
    1.17 +{
    1.18 +  protected val keywords: Map[String, String] = Map((";" -> Outer_Keyword.DIAG))
    1.19 +  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    1.20 +  lazy val completion: Completion = new Completion + symbols  // FIXME !?
    1.21 +
    1.22 +  def + (name: String, kind: String): Outer_Syntax =
    1.23 +  {
    1.24 +    val new_keywords = keywords + (name -> kind)
    1.25 +    val new_lexicon = lexicon + name
    1.26 +    val new_completion = completion + name
    1.27 +    new Outer_Syntax(symbols) {
    1.28 +      override val lexicon = new_lexicon
    1.29 +      override val keywords = new_keywords
    1.30 +      override lazy val completion = new_completion
    1.31 +    }
    1.32 +  }
    1.33 +
    1.34 +  def + (name: String): Outer_Syntax = this + (name, Outer_Keyword.MINOR)
    1.35 +
    1.36 +  def is_command(name: String): Boolean =
    1.37 +    keywords.get(name) match {
    1.38 +      case Some(kind) => kind != Outer_Keyword.MINOR
    1.39 +      case None => false
    1.40 +    }
    1.41 +
    1.42 +
    1.43 +  /* tokenize */
    1.44 +
    1.45 +  def scan(input: Reader[Char]): List[Outer_Lex.Token] =
    1.46 +  {
    1.47 +    import lexicon._
    1.48 +
    1.49 +    parseAll(rep(token(symbols, is_command)), input) match {
    1.50 +      case Success(tokens, _) => tokens
    1.51 +      case _ => error("Failed to tokenize input:\n" + input.source.toString)
    1.52 +    }
    1.53 +  }
    1.54 +
    1.55 +  def scan(input: CharSequence): List[Outer_Lex.Token] =
    1.56 +    scan(new CharSequenceReader(input))
    1.57 +}