# HG changeset patch
# User wenzelm
# Date 1283191963 -7200
# Node ID 1d5b3175fd300159c89d625cd030d4ff33817827
# Parent  682c4932b3cca83b3e4b5309a45232e4d621eacc
text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;

diff -r 682c4932b3cc -r 1d5b3175fd30 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Aug 30 20:11:21 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Aug 30 20:12:43 2010 +0200
@@ -77,9 +77,11 @@
       commands.iterator.find(_.is_unparsed) match {
         case Some(first_unparsed) =>
           val first =
-            commands.reverse_iterator(first_unparsed).find(_.is_command) getOrElse commands.head
+            commands.reverse_iterator(first_unparsed).
+              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.head
           val last =
-            commands.iterator(first_unparsed).find(_.is_command) getOrElse commands.last
+            commands.iterator(first_unparsed).
+              dropWhile(_.newlines == 0).find(_.is_command) getOrElse commands.last
           val range =
             commands.iterator(first).takeWhile(_ != last).toList ::: List(last)