src/Pure/Thy/thy_syntax.scala
changeset 56373 0605d90be6fc
parent 56372 fadb0fef09d7
child 56393 22f533e6a049
--- a/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:22:12 2014 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Apr 02 20:41:44 2014 +0200
@@ -141,9 +141,9 @@
       }
 
       val commands =
-        if (overlays.is_empty) node.command_range(perspective.range)
-        else node.command_range()
-      check_ranges(perspective.ranges, commands.toStream)
+        (if (overlays.is_empty) node.command_iterator(perspective.range)
+         else node.command_iterator()).toStream
+      check_ranges(perspective.ranges, commands)
       (Command.Perspective(visible.toList), Command.Perspective(visible_overlay.toList))
     }
   }