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))) }