Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
authorwenzelm
Mon, 30 Aug 2010 20:12:43 +0200
changeset 38878 1d5b3175fd30
parent 38877 682c4932b3cc
child 38879 dde403450419
text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;
src/Pure/Thy/thy_syntax.scala file | annotate | diff | comparison | revisions 
--- 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)
isabelle