src/Pure/PIDE/document.scala
changeset 59702 58dfaa369c11
parent 59695 a03e0561bdbf
child 60215 5fb4990dfc73
--- a/src/Pure/PIDE/document.scala	Sun Mar 15 14:46:01 2015 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Mar 15 19:21:15 2015 +0100
@@ -256,6 +256,8 @@
       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