# HG changeset patch
# User wenzelm
# Date 1285187121 -7200
# Node ID 20bba9cc4b519d852df11f7cbe45ffa0e1e405a3
# Parent  ff694044a55b999111ff24df7e0f1ce430f01ca6
Snapshot.convert/revert: explicit error report to isolate sporadic crash;

diff -r ff694044a55b -r 20bba9cc4b51 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Sep 22 22:15:36 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 22 22:25:21 2010 +0200
@@ -305,10 +305,18 @@
         def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
 
         def convert(range: Text.Range): Text.Range =
-          if (edits.isEmpty) range else range.map(convert(_))
+          try { if (edits.isEmpty) range else range.map(convert(_)) }
+          catch { // FIXME tmp
+            case e: IllegalArgumentException =>
+              System.err.println((true, range, edits)); throw(e)
+          }
 
         def revert(range: Text.Range): Text.Range =
-          if (edits.isEmpty) range else range.map(revert(_))
+          try { if (edits.isEmpty) range else range.map(revert(_)) }
+          catch { // FIXME tmp
+            case e: IllegalArgumentException =>
+              System.err.println((false, range, reverse_edits)); throw(e)
+          }
 
         def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
           : Stream[Text.Info[Option[A]]] =