tuned comments;
authorwenzelm
Sat Nov 03 19:31:50 2018 +0100 (6 months ago)
changeset 69224fe9d746b273e
parent 69223 44d68a00917c
child 69225 bf2fecda8383
tuned comments;
src/Pure/PIDE/xml.ML
     1.1 --- a/src/Pure/PIDE/xml.ML	Sat Nov 03 19:31:15 2018 +0100
     1.2 +++ b/src/Pure/PIDE/xml.ML	Sat Nov 03 19:31:50 2018 +0100
     1.3 @@ -93,7 +93,7 @@
     1.4    | unwrap_elem _ = NONE;
     1.5  
     1.6  
     1.7 -(* text context *)
     1.8 +(* text content *)
     1.9  
    1.10  fun add_content tree =
    1.11    (case unwrap_elem tree of