changeset 64800 | 415dafeb9669 |
parent 64763 | 20e498a28f5e |
child 64806 | 99f49258b02b |
--- a/src/Pure/PIDE/line.scala Thu Jan 05 12:23:25 2017 +0100 +++ b/src/Pure/PIDE/line.scala Thu Jan 05 15:15:51 2017 +0100 @@ -136,6 +136,12 @@ else ((0 /: lines) { case (n, line) => n + line.text.length + 1 }) - 1 def full_range: Text.Range = Text.Range(0, length) + + lazy val blob: (Bytes, Symbol.Text_Chunk) = + { + val text = make_text + (Bytes(text), Symbol.Text_Chunk(text)) + } }