author | wenzelm |
Tue, 05 Mar 2019 16:46:42 +0100 | |
changeset 69869 | f2c3512df446 |
parent 69868 | ab993a273def |
child 69870 | 0af6b4a5a7d9 |
--- a/src/Pure/Isar/document_structure.scala Tue Mar 05 19:33:40 2019 +0100 +++ b/src/Pure/Isar/document_structure.scala Tue Mar 05 16:46:42 2019 +0100 @@ -24,6 +24,9 @@ command.span.is_kind(keywords, kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false) + def is_heading_command(command: Command): Boolean = + proper_heading_level(command).isDefined + def proper_heading_level(command: Command): Option[Int] = command.span.name match { case Thy_Header.CHAPTER => Some(0)