changeset 73556 | 192bcee4f8b8 |
parent 70997 | 325247f32da9 |
child 73570 | e21aef453cd4 |
--- a/src/Pure/PIDE/xml.ML Sat Apr 10 20:22:07 2021 +0200 +++ b/src/Pure/PIDE/xml.ML Sat Apr 10 21:50:59 2021 +0200 @@ -35,6 +35,7 @@ | Text of string type body = tree list val blob: string list -> body + val chunk: body -> tree val is_empty: tree -> bool val is_empty_body: body -> bool val xml_elemN: string @@ -79,6 +80,8 @@ val blob = map Text; +fun chunk body = Elem (Markup.empty, body); + fun is_empty (Text "") = true | is_empty _ = false;