# HG changeset patch
# User wenzelm
# Date 1551640405 -3600
# Node ID e18ba60a1cf8cc5278993467746aa007b5cdb16e
# Parent  3d0f27273aa1c1d3489eb5c569e77cabb1e2c24f
clarified signature -- allow more re-use;

diff -r 3d0f27273aa1 -r e18ba60a1cf8 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Sun Mar 03 19:30:17 2019 +0100
+++ b/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:13:25 2019 +0100
@@ -20,10 +20,24 @@
   { val length: Int = (0 /: body)(_ + _.length) }
   case class Atom(length: Int) extends Document
 
-  private def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
+  def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
     command.span.is_kind(keywords,
       kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
 
+  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
+  {
+    command.span.name match {
+      case Thy_Header.CHAPTER => Some(0)
+      case Thy_Header.SECTION => Some(1)
+      case Thy_Header.SUBSECTION => Some(2)
+      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
+    }
+  }
+
 
 
   /** context blocks **/
@@ -137,19 +151,7 @@
   {
     override def name: String = command.span.name
     override def source: String = command.source
-    override def heading_level: Option[Int] =
-    {
-      name match {
-        case Thy_Header.CHAPTER => Some(0)
-        case Thy_Header.SECTION => Some(1)
-        case Thy_Header.SUBSECTION => Some(2)
-        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
-      }
-    }
+    override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command)
   }
 
   def parse_sections(