diff -r eeba70379f1a -r 0a5612040a8b src/Pure/PIDE/document.scala --- a/src/Pure/PIDE/document.scala Fri Jun 17 14:35:24 2011 +0200 +++ b/src/Pure/PIDE/document.scala Fri Jun 17 23:18:22 2011 +0200 @@ -307,20 +307,8 @@ def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i)) def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i)) - - def convert(range: Text.Range): Text.Range = - 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 = - 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 convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r)) + def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r)) def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A]) : Stream[Text.Info[Option[A]]] =