src/Pure/Isar/outer_syntax.scala
changeset 40458 12c8c64203b3
parent 40455 e035dad8eca2
child 40459 913e545d9a9b
equal deleted inserted replaced
40457:3b0050718b31 40458:12c8c64203b3
    31   }
    31   }
    32 
    32 
    33   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    33   def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    34 
    34 
    35   def is_command(name: String): Boolean =
    35   def is_command(name: String): Boolean =
    36     keywords.get(name) match {
    36     keyword_kind(name) match {
    37       case Some(kind) => kind != Keyword.MINOR
    37       case Some(kind) => kind != Keyword.MINOR
    38       case None => false
    38       case None => false
    39     }
    39     }
    40 
    40 
    41   def is_heading(name: String): Boolean =
    41   def is_heading(name: String): Boolean =
    42     keywords.get(name) match {
    42     keyword_kind(name) match {
    43       case Some(kind) => Keyword.heading(kind)
    43       case Some(kind) => Keyword.heading(kind)
    44       case None => false
    44       case None => false
    45     }
    45     }
    46 
    46 
    47   def heading_level(name: String): Option[Int] =
    47   def heading_level(name: String): Option[Int] =
    48     name match {
    48     name match {
    49       // FIXME avoid hard-wired info
    49       // FIXME avoid hard-wired info!?
    50       case "header" => Some(1)
    50       case "header" => Some(1)
    51       case "chapter" => Some(2)
    51       case "chapter" => Some(2)
    52       case "section" | "sect" => Some(3)
    52       case "section" | "sect" => Some(3)
    53       case "subsection" | "subsect" => Some(4)
    53       case "subsection" | "subsect" => Some(4)
    54       case "subsubsection" | "subsubsect" => Some(5)
    54       case "subsubsection" | "subsubsect" => Some(5)
    55       case _ => None
    55       case _ =>
       
    56         keyword_kind(name) match {
       
    57           case Some(kind) if Keyword.theory(kind) => Some(6)
       
    58           case _ => None
       
    59         }
    56     }
    60     }
    57 
    61 
    58   def heading_level(command: Command): Option[Int] =
    62   def heading_level(command: Command): Option[Int] =
    59     heading_level(command.name)
    63     heading_level(command.name)
    60 
    64