src/Pure/Isar/outer_syntax.scala
changeset 40458 12c8c64203b3
parent 40455 e035dad8eca2
child 40459 913e545d9a9b
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:42:20 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:43:06 2010 +0100
     1.3 @@ -33,26 +33,30 @@
     1.4    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
     1.5  
     1.6    def is_command(name: String): Boolean =
     1.7 -    keywords.get(name) match {
     1.8 +    keyword_kind(name) match {
     1.9        case Some(kind) => kind != Keyword.MINOR
    1.10        case None => false
    1.11      }
    1.12  
    1.13    def is_heading(name: String): Boolean =
    1.14 -    keywords.get(name) match {
    1.15 +    keyword_kind(name) match {
    1.16        case Some(kind) => Keyword.heading(kind)
    1.17        case None => false
    1.18      }
    1.19  
    1.20    def heading_level(name: String): Option[Int] =
    1.21      name match {
    1.22 -      // FIXME avoid hard-wired info
    1.23 +      // FIXME avoid hard-wired info!?
    1.24        case "header" => Some(1)
    1.25        case "chapter" => Some(2)
    1.26        case "section" | "sect" => Some(3)
    1.27        case "subsection" | "subsect" => Some(4)
    1.28        case "subsubsection" | "subsubsect" => Some(5)
    1.29 -      case _ => None
    1.30 +      case _ =>
    1.31 +        keyword_kind(name) match {
    1.32 +          case Some(kind) if Keyword.theory(kind) => Some(6)
    1.33 +          case _ => None
    1.34 +        }
    1.35      }
    1.36  
    1.37    def heading_level(command: Command): Option[Int] =