changeset 73028 | 95e0f014cd24 |
parent 71601 | 97ccf48c2f0c |
child 73029 | 64157cae1ba4 |
--- a/src/Pure/PIDE/yxml.scala Sat Jan 02 16:12:52 2021 +0100 +++ b/src/Pure/PIDE/yxml.scala Sat Jan 02 16:30:43 2021 +0100 @@ -125,7 +125,7 @@ def parse(source: CharSequence): XML.Tree = parse_body(source) match { case List(result) => result - case Nil => XML.Text("") + case Nil => XML.no_text case _ => err("multiple XML trees") }