Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuned signature;
authorwenzelm
Sun, 03 Mar 2019 20:27:42 +0100
changeset 69860 b58a575d211e
parent 69859 e18ba60a1cf8
child 69861 62e47f06d22c
child 69862 db622ada496d
tuned signature;
src/Pure/Isar/document_structure.scala file | annotate | diff | comparison | revisions 
--- 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)
isabelle