more direct Linear_Set.reverse, swapping orientation of the graph;
tuned;

--- a/src/Pure/General/linear_set.scala	Thu Aug 09 17:13:46 2012 +0200
+++ b/src/Pure/General/linear_set.scala	Thu Aug 09 19:37:42 2012 +0200
@@ -34,6 +34,8 @@
 {
   override def companion: GenericCompanion[Linear_Set] = Linear_Set
 
+  def reverse: Linear_Set[A] = new Linear_Set(end, start, prevs, nexts)
+
 
   /* relative addressing */
 
@@ -132,26 +134,22 @@
   def contains(elem: A): Boolean =
     !isEmpty && (end.get == elem || nexts.isDefinedAt(elem))
 
-  private def make_iterator(from: Option[A], which: Map[A, A]): Iterator[A] = new Iterator[A] {
+  private def make_iterator(from: Option[A]): Iterator[A] = new Iterator[A] {
     private var next_elem = from
     def hasNext(): Boolean = next_elem.isDefined
     def next(): A =
       next_elem match {
         case Some(elem) =>
-          next_elem = which.get(elem)
+          next_elem = nexts.get(elem)
           elem
         case None => Iterator.empty.next()
       }
   }
 
-  override def iterator: Iterator[A] = make_iterator(start, nexts)
+  override def iterator: Iterator[A] = make_iterator(start)
 
   def iterator(elem: A): Iterator[A] =
-    if (contains(elem)) make_iterator(Some(elem), nexts)
-    else throw new Linear_Set.Undefined(elem)
-
-  def reverse_iterator(elem: A): Iterator[A] =
-    if (contains(elem)) make_iterator(Some(elem), prevs)
+    if (contains(elem)) make_iterator(Some(elem))
     else throw new Linear_Set.Undefined(elem)
 
   def + (elem: A): Linear_Set[A] = insert_after(end, elem)

--- a/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 17:13:46 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Thu Aug 09 19:37:42 2012 +0200
@@ -196,41 +196,42 @@
 
   /* phase 2: recover command spans */
 
-  @tailrec private def recover_spans(
+  private def recover_spans(
     syntax: Outer_Syntax,
     node_name: Document.Node.Name,
-    commands: Linear_Set[Command]): Linear_Set[Command] =
+    old_commands: Linear_Set[Command]): Linear_Set[Command] =
   {
-    commands.iterator.find(cmd => !cmd.is_defined) match {
-      case Some(first_undefined) =>
-        val first =
-          commands.reverse_iterator(first_undefined).
-            dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
-        val last =
-          commands.iterator(first_undefined).
-            dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
-        val range =
-          commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
+    def bound(commands: Linear_Set[Command], cmd: Command): Command =
+      commands.iterator(cmd).dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
 
-        val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
+    @tailrec def recover(commands: Linear_Set[Command]): Linear_Set[Command] =
+      commands.iterator.find(cmd => !cmd.is_defined) match {
+        case Some(first_undefined) =>
+          val first = bound(commands.reverse, first_undefined)
+          val last = bound(commands, first_undefined)
+          val range =
+            commands.iterator(first).takeWhile(_ != last).toList ::: List(last)
+
+          val spans0 = parse_spans(syntax.scan(range.map(_.source).mkString))
 
-        val (before_edit, spans1) =
-          if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
-            (Some(first), spans0.tail)
-          else (commands.prev(first), spans0)
+          val (before_edit, spans1) =
+            if (!spans0.isEmpty && first.is_command && first.span == spans0.head)
+              (Some(first), spans0.tail)
+            else (commands.prev(first), spans0)
 
-        val (after_edit, spans2) =
-          if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
-            (Some(last), spans1.take(spans1.length - 1))
-          else (commands.next(last), spans1)
+          val (after_edit, spans2) =
+            if (!spans1.isEmpty && last.is_command && last.span == spans1.last)
+              (Some(last), spans1.take(spans1.length - 1))
+            else (commands.next(last), spans1)
 
-        val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
-        val new_commands =
-          commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
-        recover_spans(syntax, node_name, new_commands)
+          val inserted = spans2.map(span => Command(Document.new_id(), node_name, span))
+          val new_commands =
+            commands.delete_between(before_edit, after_edit).append_after(before_edit, inserted)
+          recover(new_commands)
 
-      case None => commands
-    }
+        case None => commands
+      }
+    recover(old_commands)
   }