src/Pure/Thy/present.scala
changeset 67251 573077aa2826
parent 67247 3a9651318015
child 67253 93b4333f33bb
--- a/src/Pure/Thy/present.scala	Thu Dec 21 22:56:51 2017 +0100
+++ b/src/Pure/Thy/present.scala	Fri Dec 22 11:39:49 2017 +0100
@@ -134,7 +134,7 @@
   /* text document */
 
   def text_document(snapshot: Document.Snapshot): XML.Body =
-    snapshot.node.get_text match {
+    snapshot.node.source match {
       case "" => Nil
       case txt => List(XML.Text(Symbol.decode(txt)))
     }