# HG changeset patch
# User wenzelm
# Date 1551800802 -3600
# Node ID f2c3512df446a5b313786f59390fac120c58ccd5
# Parent  ab993a273defa6dc7be93af31a795cd13481d8c2
tuned signature;

diff -r ab993a273def -r f2c3512df446 src/Pure/Isar/document_structure.scala
--- 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)