# HG changeset patch
# User wenzelm
# Date 1535538119 -7200
# Node ID 51ab4c78235b443c4e91d7b35b16e8cb48128677
# Parent  d8251a61cce8f3934173d2e7e074d732ef8f43c8
tuned signature;

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
       }
     }
diff -r d8251a61cce8 -r 51ab4c78235b src/Pure/PIDE/command_span.scala
--- a/src/Pure/PIDE/command_span.scala	Wed Aug 29 11:44:28 2018 +0200
+++ b/src/Pure/PIDE/command_span.scala	Wed Aug 29 12:21:59 2018 +0200
@@ -39,6 +39,12 @@
         case _ => start
       }
 
+    def is_kind(keywords: Keyword.Keywords, pred: String => Boolean): Boolean =
+      keywords.kinds.get(name) match {
+        case Some(k) => pred(k)
+        case None => false
+      }
+
     def is_begin: Boolean = content.exists(_.is_begin)
     def is_end: Boolean = content.exists(_.is_end)