more explicit error message;
authorwenzelm
Fri Jun 17 23:18:22 2011 +0200 (2011-06-17)
changeset 434250a5612040a8b
parent 43424 eeba70379f1a
child 43426 24e2e2f0032b
more explicit error message;
convert/revert range;
tuned;
src/Pure/PIDE/document.scala
src/Pure/PIDE/text.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Jun 17 14:35:24 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Jun 17 23:18:22 2011 +0200
     1.3 @@ -307,20 +307,8 @@
     1.4  
     1.5          def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
     1.6          def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
     1.7 -
     1.8 -        def convert(range: Text.Range): Text.Range =
     1.9 -          try { if (edits.isEmpty) range else range.map(convert(_)) }
    1.10 -          catch { // FIXME tmp
    1.11 -            case e: IllegalArgumentException =>
    1.12 -              System.err.println((true, range, edits)); throw(e)
    1.13 -          }
    1.14 -
    1.15 -        def revert(range: Text.Range): Text.Range =
    1.16 -          try { if (edits.isEmpty) range else range.map(revert(_)) }
    1.17 -          catch { // FIXME tmp
    1.18 -            case e: IllegalArgumentException =>
    1.19 -              System.err.println((false, range, reverse_edits)); throw(e)
    1.20 -          }
    1.21 +        def convert(range: Text.Range) = (range /: edits)((r, edit) => edit.convert(r))
    1.22 +        def revert(range: Text.Range) = (range /: reverse_edits)((r, edit) => edit.revert(r))
    1.23  
    1.24          def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
    1.25            : Stream[Text.Info[Option[A]]] =
     2.1 --- a/src/Pure/PIDE/text.scala	Fri Jun 17 14:35:24 2011 +0200
     2.2 +++ b/src/Pure/PIDE/text.scala	Fri Jun 17 23:18:22 2011 +0200
     2.3 @@ -25,7 +25,8 @@
     2.4    sealed case class Range(val start: Offset, val stop: Offset)
     2.5    {
     2.6      // denotation: {start} Un {i. start < i & i < stop}
     2.7 -    require(start <= stop)
     2.8 +    if (start > stop)
     2.9 +      error("Bad range: [" + start.toString + ":" + stop.toString + "]")
    2.10  
    2.11      override def toString = "[" + start.toString + ":" + stop.toString + "]"
    2.12  
    2.13 @@ -71,11 +72,13 @@
    2.14  
    2.15      private def transform(do_insert: Boolean, i: Offset): Offset =
    2.16        if (i < start) i
    2.17 -      else if (is_insert == do_insert) i + text.length
    2.18 +      else if (do_insert) i + text.length
    2.19        else (i - text.length) max start
    2.20  
    2.21 -    def convert(i: Offset): Offset = transform(true, i)
    2.22 -    def revert(i: Offset): Offset = transform(false, i)
    2.23 +    def convert(i: Offset): Offset = transform(is_insert, i)
    2.24 +    def revert(i: Offset): Offset = transform(!is_insert, i)
    2.25 +    def convert(range: Range): Range = range.map(convert)
    2.26 +    def revert(range: Range): Range = range.map(revert)
    2.27  
    2.28  
    2.29      /* edit strings */