--- a/src/Pure/Thy/thy_syntax.scala Mon Aug 11 22:46:27 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Mon Aug 11 22:59:38 2014 +0200
@@ -332,8 +332,8 @@
val visible = perspective.commands.toSet
def next_invisible_command(cmds: Linear_Set[Command], from: Command): Command =
- cmds.iterator(from).dropWhile(cmd => !cmd.is_command || visible(cmd))
- .find(_.is_command) getOrElse cmds.last
+ cmds.iterator(from).dropWhile(cmd => !cmd.is_proper || visible(cmd))
+ .find(_.is_proper) getOrElse cmds.last
@tailrec def recover(cmds: Linear_Set[Command]): Linear_Set[Command] =
cmds.find(_.is_unparsed) match {