# HG changeset patch
# User wenzelm
# Date 1218233371 -7200
# Node ID b96c73f11a23bffd9c6e0185888f2aa77bcfb2fb
# Parent  9861b39a2fd5fef8f8a3686bf525b6da6fed8c9b
YXML.parse: allow text without markup, potentially empty;

diff -r 9861b39a2fd5 -r b96c73f11a23 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Sat Aug 09 00:09:29 2008 +0200
+++ b/src/Pure/General/yxml.ML	Sat Aug 09 00:09:31 2008 +0200
@@ -119,8 +119,9 @@
 
 fun parse source =
   (case parse_body source of
-    [result as XML.Elem _] => result
-  | _ => err "no root element");
+    [result] => result
+  | [] => XML.Text ""
+  | _ => err "multiple results");
 
 val parse_element = parse #> (fn XML.Elem elem => elem);