--- a/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Feb 01 13:38:51 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/ProofDocument.scala Sun Feb 01 13:57:59 2009 +0100
@@ -229,11 +229,13 @@
val structural_changes = new EventBus[StructureChange]
- def commands = new Iterator[Command] {
- var current = first_token
+ def commands_from(start: Token) = new Iterator[Command] {
+ var current = start
def hasNext = current != null
- def next() = { val s = current.command ; current = s.last.next ; s }
+ def next = { val s = current.command ; current = s.last.next ; s }
}
+ def commands_from(start: Command): Iterator[Command] = commands_from(start.first)
+ def commands = commands_from(first_token)
def find_command_at(pos: Int): Command = {
for (cmd <- commands) { if (pos < cmd.stop) return cmd }