# HG changeset patch
# User wenzelm
# Date 1555161255 -7200
# Node ID 5e60443f5ad4d6e2e141abbc2c23ad1d57bda7b0
# Parent  1657688a64060cc78820070186bf5e164897a250# Parent  73a34cb9e67ef2088d3fa9c169b5b48e21733a61
merged

diff -r 1657688a6406 -r 5e60443f5ad4 src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Sat Apr 13 08:43:33 2019 +0000
+++ b/src/Pure/Isar/document_structure.scala	Sat Apr 13 15:14:15 2019 +0200
@@ -24,6 +24,9 @@
     command.span.is_kind(keywords,
       kind => Keyword.theory(kind) && !Keyword.theory_end(kind), false)
 
+  def is_document_command(keywords: Keyword.Keywords, command: Command): Boolean =
+    command.span.is_kind(keywords, Keyword.document, false)
+
   def is_heading_command(command: Command): Boolean =
     proper_heading_level(command).isDefined