src/Pure/PIDE/line.scala
changeset 64701 931f51fb24ca
parent 64689 f32efd2eeb2c
child 64763 20e498a28f5e
equal deleted inserted replaced
64700:14deaeaa6476 64701:931f51fb24ca
   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 
   134 
   135     lazy val end_offset: Text.Offset =
   135     lazy val length: Int =
   136       if (lines.isEmpty) 0
   136       if (lines.isEmpty) 0
   137       else ((0 /: lines) { case (n, line) => n + text_length(line.text) + 1 }) - 1
   137       else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
   138 
   138 
   139     def full_range: Text.Range = Text.Range(0, end_offset)
   139     def full_range: Text.Range = Text.Range(0, length)
   140   }
   140   }
   141 
   141 
   142 
   142 
   143   /* line text */
   143   /* line text */
   144 
   144