# HG changeset patch
# User wenzelm
# Date 1541269910 -3600
# Node ID fe9d746b273ef9d931289a4bb1c8f741427511e7
# Parent  44d68a00917c1e6fa0d465dbfe93b02550f885d3
tuned comments;

diff -r 44d68a00917c -r fe9d746b273e src/Pure/PIDE/xml.ML
--- 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