# HG changeset patch
# User immler@in.tum.de
# Date 1233493079 -3600
# Node ID 73225f520f8cededd4396ea2232bd3a1ac9ade15
# Parent  3be515f1379d054e544ec2cdb72b74b2e7e13e25
more flexible commands-iterators

diff -r 3be515f1379d -r 73225f520f8c src/Tools/jEdit/src/proofdocument/ProofDocument.scala
--- 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 }