src/Pure/Isar/outer_syntax.scala
author wenzelm
Tue, 17 Aug 2010 22:57:11 +0200
changeset 38471 0924654b8163
parent 36956 21be4832c362
child 40454 2516ea25a54b
permissions -rw-r--r--
report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/Isar/outer_syntax.scala
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     3
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     4
Isabelle/Isar outer syntax.
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     5
*/
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     6
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     7
package isabelle
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     8
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
     9
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    10
import scala.util.parsing.input.{Reader, CharSequenceReader}
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    11
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    12
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    13
class Outer_Syntax(symbols: Symbol.Interpretation)
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    14
{
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 34264
diff changeset
    15
  protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    16
  protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    17
  lazy val completion: Completion = new Completion + symbols  // FIXME !?
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    18
38471
0924654b8163 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
wenzelm
parents: 36956
diff changeset
    19
  def keyword_kind(name: String): Option[String] = keywords.get(name)
0924654b8163 report command token name instead of kind, which can be retrieved later via Outer_Syntax.keyword_kind;
wenzelm
parents: 36956
diff changeset
    20
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    21
  def + (name: String, kind: String): Outer_Syntax =
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    22
  {
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    23
    val new_keywords = keywords + (name -> kind)
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    24
    val new_lexicon = lexicon + name
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    25
    val new_completion = completion + name
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    26
    new Outer_Syntax(symbols) {
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    27
      override val lexicon = new_lexicon
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    28
      override val keywords = new_keywords
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    29
      override lazy val completion = new_completion
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    30
    }
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    31
  }
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    32
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 34264
diff changeset
    33
  def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    34
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    35
  def is_command(name: String): Boolean =
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    36
    keywords.get(name) match {
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 34264
diff changeset
    37
      case Some(kind) => kind != Keyword.MINOR
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    38
      case None => false
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    39
    }
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    40
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    41
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    42
  /* tokenize */
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    43
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36947
diff changeset
    44
  def scan(input: Reader[Char]): List[Token] =
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    45
  {
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    46
    import lexicon._
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    47
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    48
    parseAll(rep(token(symbols, is_command)), input) match {
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    49
      case Success(tokens, _) => tokens
34264
b5025782a4ed tuned message;
wenzelm
parents: 34166
diff changeset
    50
      case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    51
    }
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    52
  }
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    53
36956
21be4832c362 renamed class Outer_Lex to Token and Token_Kind to Token.Kind;
wenzelm
parents: 36947
diff changeset
    54
  def scan(input: CharSequence): List[Token] =
34166
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    55
    scan(new CharSequenceReader(input))
446a33b874b3 renamed class Outer_Keyword to Outer_Syntax;
wenzelm
parents:
diff changeset
    56
}