src/Pure/PIDE/line.scala
changeset 64800 415dafeb9669
parent 64763 20e498a28f5e
child 64806 99f49258b02b
equal deleted inserted replaced
64799:c0c648911f1a 64800:415dafeb9669
   134     lazy val length: Int =
   134     lazy val length: Int =
   135       if (lines.isEmpty) 0
   135       if (lines.isEmpty) 0
   136       else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
   136       else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1
   137 
   137 
   138     def full_range: Text.Range = Text.Range(0, length)
   138     def full_range: Text.Range = Text.Range(0, length)
       
   139 
       
   140     lazy val blob: (Bytes, Symbol.Text_Chunk) =
       
   141     {
       
   142       val text = make_text
       
   143       (Bytes(text), Symbol.Text_Chunk(text))
       
   144     }
   139   }
   145   }
   140 
   146 
   141 
   147 
   142   /* line text */
   148   /* line text */
   143 
   149