src/Pure/Isar/document_structure.scala
changeset 68840 51ab4c78235b
parent 64610 1b89608974e9
child 68845 3b2daa7bf9f4
--- 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
       }
     }