# HG changeset patch
# User wenzelm
# Date 1308345502 -7200
# Node ID 0a5612040a8bbdc52b56dc9a410379e76e351e95
# Parent  eeba70379f1a35d5a4ff0945c76f2d5791d428f9
more explicit error message;
convert/revert range;
tuned;

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]]] =
diff -r eeba70379f1a -r 0a5612040a8b src/Pure/PIDE/text.scala
--- a/src/Pure/PIDE/text.scala	Fri Jun 17 14:35:24 2011 +0200
+++ b/src/Pure/PIDE/text.scala	Fri Jun 17 23:18:22 2011 +0200
@@ -25,7 +25,8 @@
   sealed case class Range(val start: Offset, val stop: Offset)
   {
     // denotation: {start} Un {i. start < i & i < stop}
-    require(start <= stop)
+    if (start > stop)
+      error("Bad range: [" + start.toString + ":" + stop.toString + "]")
 
     override def toString = "[" + start.toString + ":" + stop.toString + "]"
 
@@ -71,11 +72,13 @@
 
     private def transform(do_insert: Boolean, i: Offset): Offset =
       if (i < start) i
-      else if (is_insert == do_insert) i + text.length
+      else if (do_insert) i + text.length
       else (i - text.length) max start
 
-    def convert(i: Offset): Offset = transform(true, i)
-    def revert(i: Offset): Offset = transform(false, i)
+    def convert(i: Offset): Offset = transform(is_insert, i)
+    def revert(i: Offset): Offset = transform(!is_insert, i)
+    def convert(range: Range): Range = range.map(convert)
+    def revert(range: Range): Range = range.map(revert)
 
 
     /* edit strings */