src/Pure/Isar/outer_syntax.scala
author wenzelm
Sun Apr 17 21:42:47 2011 +0200 (2011-04-17 ago)
changeset 42381 309ec68442c6
parent 40533 e38e80686ce5
child 43411 0206466ee473
permissions -rw-r--r--
added Binding.print convenience, which includes quote already;
     1 /*  Title:      Pure/Isar/outer_syntax.scala
     2     Author:     Makarius
     3 
     4 Isabelle/Isar outer syntax.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import scala.util.parsing.input.{Reader, CharSequenceReader}
    11 
    12 
    13 class Outer_Syntax(symbols: Symbol.Interpretation)
    14 {
    15   protected val keywords: Map[String, String] = Map((";" -> Keyword.DIAG))
    16   protected val lexicon: Scan.Lexicon = Scan.Lexicon.empty
    17   lazy val completion: Completion = new Completion + symbols  // FIXME !?
    18 
    19   def keyword_kind(name: String): Option[String] = keywords.get(name)
    20 
    21   def + (name: String, kind: String, replace: String): Outer_Syntax =
    22   {
    23     val new_keywords = keywords + (name -> kind)
    24     val new_lexicon = lexicon + name
    25     val new_completion = completion + (name, replace)
    26     new Outer_Syntax(symbols) {
    27       override val lexicon = new_lexicon
    28       override val keywords = new_keywords
    29       override lazy val completion = new_completion
    30     }
    31   }
    32 
    33   def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    34 
    35   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    36 
    37   def is_command(name: String): Boolean =
    38     keyword_kind(name) match {
    39       case Some(kind) => kind != Keyword.MINOR
    40       case None => false
    41     }
    42 
    43   def heading_level(name: String): Option[Int] =
    44     name match {
    45       // FIXME avoid hard-wired info!?
    46       case "header" => Some(1)
    47       case "chapter" => Some(2)
    48       case "section" | "sect" => Some(3)
    49       case "subsection" | "subsect" => Some(4)
    50       case "subsubsection" | "subsubsect" => Some(5)
    51       case _ =>
    52         keyword_kind(name) match {
    53           case Some(kind) if Keyword.theory(kind) => Some(6)
    54           case _ => None
    55         }
    56     }
    57 
    58   def heading_level(command: Command): Option[Int] =
    59     heading_level(command.name)
    60 
    61 
    62   /* tokenize */
    63 
    64   def scan(input: Reader[Char]): List[Token] =
    65   {
    66     import lexicon._
    67 
    68     parseAll(rep(token(symbols, is_command)), input) match {
    69       case Success(tokens, _) => tokens
    70       case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    71     }
    72   }
    73 
    74   def scan(input: CharSequence): List[Token] =
    75     scan(new CharSequenceReader(input))
    76 }