changeset 80820 | db114ec720cb |
parent 80563 | 36da6a3c79d6 |
child 80821 | eb383d50564b |
--- a/src/Pure/PIDE/yxml.ML Fri Sep 06 19:17:29 2024 +0200 +++ b/src/Pure/PIDE/yxml.ML Fri Sep 06 20:31:20 2024 +0200 @@ -33,7 +33,6 @@ val parse_body_bytes: Bytes.T -> XML.body val parse: string -> XML.tree val parse_bytes: Bytes.T -> XML.tree - val content_of: string -> string val is_wellformed: string -> bool end; @@ -170,8 +169,6 @@ end; -val content_of = parse_body #> XML.content_of; - fun is_wellformed s = string_of_body (parse_body s) = s handle Fail _ => false;