clarified signature -- allow more re-use;
authorwenzelm
Sun Mar 03 20:13:25 2019 +0100 (3 months ago ago)
changeset 70040e18ba60a1cf8
parent 70039 3d0f27273aa1
child 70041 b58a575d211e
clarified signature -- allow more re-use;
src/Pure/Isar/document_structure.scala
     1.1 --- a/src/Pure/Isar/document_structure.scala	Sun Mar 03 19:30:17 2019 +0100
     1.2 +++ b/src/Pure/Isar/document_structure.scala	Sun Mar 03 20:13:25 2019 +0100
     1.3 @@ -20,10 +20,24 @@
     1.4    { val length: Int = (0 /: body)(_ + _.length) }
     1.5    case class Atom(length: Int) extends Document
     1.6  
     1.7 -  private def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
     1.8 +  def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean =
     1.9      command.span.is_kind(keywords,
    1.10        kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
    1.11  
    1.12 +  def heading_level(keywords: Keyword.Keywords, command: Command): Option[Int] =
    1.13 +  {
    1.14 +    command.span.name match {
    1.15 +      case Thy_Header.CHAPTER => Some(0)
    1.16 +      case Thy_Header.SECTION => Some(1)
    1.17 +      case Thy_Header.SUBSECTION => Some(2)
    1.18 +      case Thy_Header.SUBSUBSECTION => Some(3)
    1.19 +      case Thy_Header.PARAGRAPH => Some(4)
    1.20 +      case Thy_Header.SUBPARAGRAPH => Some(5)
    1.21 +      case _ if is_theory_command(keywords, command) => Some(6)
    1.22 +      case _ => None
    1.23 +    }
    1.24 +  }
    1.25 +
    1.26  
    1.27  
    1.28    /** context blocks **/
    1.29 @@ -137,19 +151,7 @@
    1.30    {
    1.31      override def name: String = command.span.name
    1.32      override def source: String = command.source
    1.33 -    override def heading_level: Option[Int] =
    1.34 -    {
    1.35 -      name match {
    1.36 -        case Thy_Header.CHAPTER => Some(0)
    1.37 -        case Thy_Header.SECTION => Some(1)
    1.38 -        case Thy_Header.SUBSECTION => Some(2)
    1.39 -        case Thy_Header.SUBSUBSECTION => Some(3)
    1.40 -        case Thy_Header.PARAGRAPH => Some(4)
    1.41 -        case Thy_Header.SUBPARAGRAPH => Some(5)
    1.42 -        case _ if is_theory_command(keywords, command) => Some(6)
    1.43 -        case _ => None
    1.44 -      }
    1.45 -    }
    1.46 +    override def heading_level: Option[Int] = Document_Structure.heading_level(keywords, command)
    1.47    }
    1.48  
    1.49    def parse_sections(