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