--- a/src/Pure/PIDE/xml.ML Sat Nov 03 19:31:15 2018 +0100 +++ b/src/Pure/PIDE/xml.ML Sat Nov 03 19:31:50 2018 +0100 @@ -93,7 +93,7 @@ | unwrap_elem _ = NONE; -(* text context *) +(* text content *) fun add_content tree = (case unwrap_elem tree of