src/Pure/PIDE/line.scala
changeset 64688 d8f194556c70
parent 64683 c0c09b6dfbe0
child 64689 f32efd2eeb2c
equal deleted inserted replaced
64687:04806ad1e43a 64688:d8f194556c70
   129           else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
   129           else (0 /: lines.iterator.take(l - 1)) { case (n, line) => n + text_length(line.text) + 1 }
   130         text_length.offset(lines(l).text, c).map(line_offset + _)
   130         text_length.offset(lines(l).text, c).map(line_offset + _)
   131       }
   131       }
   132       else None
   132       else None
   133     }
   133     }
       
   134 
       
   135     lazy val end_offset: Text.Offset =
       
   136       if (lines.isEmpty) 0
       
   137       else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
       
   138 
       
   139     def full_range: Text.Range = Text.Range(0, end_offset)
   134   }
   140   }
   135 
   141 
   136 
   142 
   137   /* line text */
   143   /* line text */
   138 
   144