| changeset 65161 | 6af056380d0b |
| parent 65160 | 6e042537555d |
| child 65191 | 4c9c83311cad |
--- 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)