--- a/src/Pure/Isar/document_structure.scala Sun Mar 03 20:13:25 2019 +0100
+++ b/src/Pure/Isar/document_structure.scala Sun Mar 03 20:27:42 2019 +0100
@@ -24,8 +24,7 @@
command.span.is_kind(keywords,
kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
- def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
- {
+ def proper_heading_level(command: Command): Option[Int] =
command.span.name match {
case Thy_Header.CHAPTER => Some(0)
case Thy_Header.SECTION => Some(1)
@@ -33,10 +32,12 @@
case Thy_Header.SUBSUBSECTION => Some(3)
case Thy_Header.PARAGRAPH => Some(4)
case Thy_Header.SUBPARAGRAPH => Some(5)
- case _ if is_theory_command(keywords, command) => Some(6)
case _ => None
}
- }
+
+ def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+ proper_heading_level(command) orElse
+ (if (is_theory_command(keywords, command)) Some(6) else None)