src/Tools/VSCode/src/document_model.scala

--- a/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:23:38 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Sun Mar 12 14:31:29 2017 +0100
@@ -31,6 +31,7 @@
   sealed case class Content(doc: Line.Document)
   {
     override def toString: String = doc.toString
+    def text_length: Text.Offset = doc.text_length
     def text_range: Text.Range = doc.text_range
     def text: String = doc.text
     def try_get_text(range: Text.Range): Option[String] = doc.try_get_text(range)