1 /* Title: Pure/Isar/outer_syntax.scala
4 Isabelle/Isar outer syntax.
10 import scala.util.parsing.input.{Reader, CharSequenceReader}
13 class Outer_Syntax(symbols: Symbol.Interpretation)
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 !?
19 def keyword_kind(name: String): Option[String] = keywords.get(name)
21 def + (name: String, kind: String, replace: String): Outer_Syntax =
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
33 def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
35 def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
37 def is_command(name: String): Boolean =
38 keyword_kind(name) match {
39 case Some(kind) => kind != Keyword.MINOR
43 def heading_level(name: String): Option[Int] =
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)
52 keyword_kind(name) match {
53 case Some(kind) if Keyword.theory(kind) => Some(6)
58 def heading_level(command: Command): Option[Int] =
59 heading_level(command.name)
64 def scan(input: Reader[Char]): List[Token] =
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)
74 def scan(input: CharSequence): List[Token] =
75 scan(new CharSequenceReader(input))