src/Pure/Isar/outer_syntax.scala
changeset 40454 2516ea25a54b
parent 38471 0924654b8163
child 40455 e035dad8eca2
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 11:44:35 2010 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Wed Nov 10 15:00:40 2010 +0100
     1.3 @@ -38,6 +38,20 @@
     1.4        case None => false
     1.5      }
     1.6  
     1.7 +  def heading_level(name: String): Option[Int] =
     1.8 +    name match {
     1.9 +      // FIXME avoid hard-wired info
    1.10 +      case "header" => Some(1)
    1.11 +      case "chapter" => Some(2)
    1.12 +      case "section" | "sect" => Some(3)
    1.13 +      case "subsection" | "subsect" => Some(4)
    1.14 +      case "subsubsection" | "subsubsect" => Some(5)
    1.15 +      case _ => None
    1.16 +    }
    1.17 +
    1.18 +  def heading_level(command: Command): Option[Int] =
    1.19 +    heading_level(command.name)
    1.20 +
    1.21  
    1.22    /* tokenize */
    1.23