src/Pure/PIDE/line.scala
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))
+    }
   }