author | wenzelm |
Sat, 09 Aug 2008 00:09:31 +0200 | |
changeset 27798 | b96c73f11a23 |
parent 27797 | 9861b39a2fd5 |
child 27799 | 52f07d5292cd |
--- 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);