diff -r d8251a61cce8 -r 51ab4c78235b src/Pure/Isar/document_structure.scala --- a/src/Pure/Isar/document_structure.scala Wed Aug 29 11:44:28 2018 +0200 +++ b/src/Pure/Isar/document_structure.scala Wed Aug 29 12:21:59 2018 +0200 @@ -20,11 +20,8 @@ { val length: Int = (0 /: body)(_ + _.length) } case class Atom(length: Int) extends Document - private def is_theory_command(keywords: Keyword.Keywords, name: String): Boolean = - keywords.kinds.get(name) match { - case Some(kind) => Keyword.theory(kind) && !Keyword.theory_end(kind) - case None => false - } + private def is_theory_command(keywords: Keyword.Keywords, command: Command): Boolean = + command.span.is_kind(keywords, kind => Keyword.theory(kind) && !Keyword.theory_end(kind)) @@ -36,7 +33,7 @@ text: CharSequence): List[Document] = { def is_plain_theory(command: Command): Boolean = - is_theory_command(syntax.keywords, command.span.name) && + is_theory_command(syntax.keywords, command) && !command.span.is_begin && !command.span.is_end @@ -148,7 +145,7 @@ case Thy_Header.SUBSUBSECTION => Some(3) case Thy_Header.PARAGRAPH => Some(4) case Thy_Header.SUBPARAGRAPH => Some(5) - case _ if is_theory_command(keywords, name) => Some(6) + case _ if is_theory_command(keywords, command) => Some(6) case _ => None } }