--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 24 23:20:05 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Thu Aug 25 11:27:37 2011 +0200
@@ -101,7 +101,7 @@
def command_perspective(node: Document.Node, perspective: Text.Perspective): Command.Perspective =
{
- if (perspective.isEmpty) Nil
+ if (perspective.is_empty) Nil
else {
val result = new mutable.ListBuffer[Command]
@tailrec
@@ -120,8 +120,7 @@
case _ =>
}
}
- val perspective_range = Text.Range(perspective.head.start, perspective.last.stop)
- check_ranges(perspective, node.command_range(perspective_range).toStream)
+ check_ranges(perspective.ranges, node.command_range(perspective.range).toStream)
result.toList
}
}