--- a/src/Pure/General/symbol.scala Wed Nov 09 22:23:36 2016 +0100 +++ b/src/Pure/General/symbol.scala Thu Nov 10 09:43:15 2016 +0100 @@ -197,7 +197,7 @@ } - /* text chunks */ + /* symbolic text chunks -- without actual text */ object Text_Chunk {