src/Pure/Isar/outer_syntax.scala
author wenzelm
Wed Nov 10 15:00:40 2010 +0100 (2010-11-10)
changeset 40454 2516ea25a54b
parent 38471 0924654b8163
child 40455 e035dad8eca2
permissions -rw-r--r--
some support for nested source structure, based on section headings;
     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): Outer_Syntax =
    22   {
    23     val new_keywords = keywords + (name -> kind)
    24     val new_lexicon = lexicon + name
    25     val new_completion = completion + name
    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): Outer_Syntax = this + (name, Keyword.MINOR)
    34 
    35   def is_command(name: String): Boolean =
    36     keywords.get(name) match {
    37       case Some(kind) => kind != Keyword.MINOR
    38       case None => false
    39     }
    40 
    41   def heading_level(name: String): Option[Int] =
    42     name match {
    43       // FIXME avoid hard-wired info
    44       case "header" => Some(1)
    45       case "chapter" => Some(2)
    46       case "section" | "sect" => Some(3)
    47       case "subsection" | "subsect" => Some(4)
    48       case "subsubsection" | "subsubsect" => Some(5)
    49       case _ => None
    50     }
    51 
    52   def heading_level(command: Command): Option[Int] =
    53     heading_level(command.name)
    54 
    55 
    56   /* tokenize */
    57 
    58   def scan(input: Reader[Char]): List[Token] =
    59   {
    60     import lexicon._
    61 
    62     parseAll(rep(token(symbols, is_command)), input) match {
    63       case Success(tokens, _) => tokens
    64       case _ => error("Unexpected failure of tokenizing input:\n" + input.source.toString)
    65     }
    66   }
    67 
    68   def scan(input: CharSequence): List[Token] =
    69     scan(new CharSequenceReader(input))
    70 }