src/Pure/Isar/outer_syntax.scala
changeset 58868 c5e1cce7ace3
parent 58853 f8715e7c1be6
child 58899 0a793c580685
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 13:26:20 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Nov 02 15:27:37 2014 +0100
     1.3 @@ -277,14 +277,16 @@
     1.4  
     1.5    def heading_level(command: Command): Option[Int] =
     1.6    {
     1.7 -    keyword_kind(command.name) match {
     1.8 -      case _ if command.name == "header" => Some(0)
     1.9 -      case Some(Keyword.THY_HEADING1) => Some(1)
    1.10 -      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
    1.11 -      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
    1.12 -      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
    1.13 -      case Some(kind) if Keyword.theory(kind) => Some(5)
    1.14 -      case _ => None
    1.15 +    command.name match {
    1.16 +      case "chapter" => Some(0)
    1.17 +      case "section" | "header" => Some(1)
    1.18 +      case "subsection" => Some(2)
    1.19 +      case "subsubsection" => Some(3)
    1.20 +      case _ =>
    1.21 +        keyword_kind(command.name) match {
    1.22 +          case Some(kind) if Keyword.theory(kind) => Some(4)
    1.23 +          case _ => None
    1.24 +        }
    1.25      }
    1.26    }
    1.27