1.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Mar 16 20:45:47 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Mar 16 21:20:23 2012 +0100
     1.3 @@ -68,19 +68,17 @@
     1.4      }
     1.5  
     1.6    def heading_level(name: String): Option[Int] =
     1.7 -    name match {
     1.8 -      // FIXME avoid hard-wired info!?
     1.9 -      case "header" => Some(1)
    1.10 -      case "chapter" => Some(2)
    1.11 -      case "section" | "sect" => Some(3)
    1.12 -      case "subsection" | "subsect" => Some(4)
    1.13 -      case "subsubsection" | "subsubsect" => Some(5)
    1.14 -      case _ =>
    1.15 -        keyword_kind(name) match {
    1.16 -          case Some(kind) if Keyword.theory(kind) => Some(6)
    1.17 -          case _ => None
    1.18 -        }
    1.19 +  {
    1.20 +    keyword_kind(name) match {
    1.21 +      case _ if name == "header" => Some(0)
    1.22 +      case Some(Keyword.THY_HEADING1) => Some(1)
    1.23 +      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
    1.24 +      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
    1.25 +      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
    1.26 +      case Some(kind) if Keyword.theory(kind) => Some(5)
    1.27 +      case _ => None
    1.28      }
    1.29 +  }
    1.30  
    1.31    def heading_level(command: Command): Option[Int] =
    1.32      heading_level(command.name)