tuned signature;
authorwenzelm
Sun Mar 03 20:27:42 2019 +0100 (3 months ago ago)
changeset 70041b58a575d211e
parent 70040 e18ba60a1cf8
child 70042 62e47f06d22c
child 70043 db622ada496d
tuned signature;
src/Pure/Isar/document_structure.scala
     1.1 --- a/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:13:25 2019 +0100
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:27:42 2019 +0100
     1.3 @@ -24,8 +24,7 @@
     1.4      command.span.is_kind(keywords,
     1.5        kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
     1.6  
     1.7 -  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
     1.8 -  {
     1.9 +  def proper_heading_level(command: Command): Option[Int] =
    1.10      command.span.name match {
    1.11        case Thy_Header.CHAPTER => Some(0)
    1.12        case Thy_Header.SECTION => Some(1)
    1.13 @@ -33,10 +32,12 @@
    1.14        case Thy_Header.SUBSUBSECTION => Some(3)
    1.15        case Thy_Header.PARAGRAPH => Some(4)
    1.16        case Thy_Header.SUBPARAGRAPH => Some(5)
    1.17 -      case _ if is_theory_command(keywords, command) => Some(6)
    1.18        case _ => None
    1.19      }
    1.20 -  }
    1.21 +
    1.22 +  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.23 +    proper_heading_level(command) orElse
    1.24 +      (if (is_theory_command(keywords, command)) Some(6) else None)
    1.25  
    1.26  
    1.27