# HG changeset patch
# User wenzelm
# Date 1555161223 -7200
# Node ID 73a34cb9e67ef2088d3fa9c169b5b48e21733a61
# Parent  0cc7fe6169245fdc897c2e7c1b44c78882403023
tuned signature: more operations;

diff -r 0cc7fe616924 -r 73a34cb9e67e src/Pure/Isar/document_structure.scala
--- a/src/Pure/Isar/document_structure.scala	Sat Apr 13 13:30:02 2019 +0200
+++ b/src/Pure/Isar/document_structure.scala	Sat Apr 13 15:13:43 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