src/Pure/Isar/outer_syntax.scala
changeset 59735 24bee1b11fce
parent 59702 58dfaa369c11
child 59924 801b979ec0c2
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 09:22:21 2015 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Mar 17 15:21:41 2015 +0100
     1.3 @@ -123,9 +123,7 @@
     1.4      }
     1.5  
     1.6  
     1.7 -  /* command categories */
     1.8 -
     1.9 -  def is_theory_begin(name: String): Boolean = keywords.is_command_kind(name, Keyword.theory_begin)
    1.10 +  /* load commands */
    1.11  
    1.12    def load_command(name: String): Option[List[String]] = keywords.load_command(name)
    1.13    def load_commands_in(text: String): Boolean = keywords.load_commands_in(text)
    1.14 @@ -230,13 +228,14 @@
    1.15  
    1.16    def heading_level(command: Command): Option[Int] =
    1.17    {
    1.18 -    command.name match {
    1.19 -      case "chapter" => Some(0)
    1.20 -      case "section" | "header" => Some(1)
    1.21 -      case "subsection" => Some(2)
    1.22 -      case "subsubsection" => Some(3)
    1.23 +    val name = command.span.name
    1.24 +    name match {
    1.25 +      case Thy_Header.CHAPTER => Some(0)
    1.26 +      case Thy_Header.SECTION | Thy_Header.HEADER => Some(1)
    1.27 +      case Thy_Header.SUBSECTION => Some(2)
    1.28 +      case Thy_Header.SUBSUBSECTION => Some(3)
    1.29        case _ =>
    1.30 -        keywords.command_kind(command.name) match {
    1.31 +        keywords.command_kind(name) match {
    1.32            case Some(kind) if Keyword.theory(kind) && !Keyword.theory_end(kind) => Some(4)
    1.33            case _ => None
    1.34          }
    1.35 @@ -258,7 +257,7 @@
    1.36      {
    1.37        stack match {
    1.38          case (lev, command, body) :: (_, _, body2) :: rest if level(lev) =>
    1.39 -          body2 += Outer_Syntax.Document_Block(command.name, command.source, body.toList)
    1.40 +          body2 += Outer_Syntax.Document_Block(command.span.name, command.source, body.toList)
    1.41            stack = stack.tail
    1.42            close(level)
    1.43          case _ =>