# HG changeset patch
# User wenzelm
# Date 1489069245 -3600
# Node ID 6af056380d0bcdbd35277e1cc1589be27cc4f621
# Parent  6e042537555d9235f898df3a85ec3c97de6c8263
clarified;

diff -r 6e042537555d -r 6af056380d0b src/Tools/VSCode/src/document_model.scala
--- a/src/Tools/VSCode/src/document_model.scala	Thu Mar 09 15:19:24 2017 +0100
+++ b/src/Tools/VSCode/src/document_model.scala	Thu Mar 09 15:20:45 2017 +0100
@@ -30,6 +30,7 @@
 
   sealed case class Content(doc: Line.Document)
   {
+    override def toString: String = doc.toString
     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)