src/Pure/PIDE/document.scala

       get_blob.isEmpty &&
       header == Node.no_header &&
       text_perspective.is_empty &&
       Node.is_no_perspective_command(perspective) &&
       commands.isEmpty
+
+    def has_header: Boolean = header != Node.no_header
 
     def commands: Linear_Set[Command] = _commands.commands
     def load_commands: List[Command] = _commands.load_commands
 
     def clear: Node = new Node(header = header, syntax = syntax)