diff -r fa5476c54731 -r 56247fdb8bbb src/Pure/Tools/update_comments.scala --- a/src/Pure/Tools/update_comments.scala Mon Dec 06 15:10:15 2021 +0100 +++ b/src/Pure/Tools/update_comments.scala Mon Dec 06 15:34:54 2021 +0100 @@ -23,7 +23,7 @@ case tok :: rest if tok.source == "--" || tok.source == Symbol.comment => rest.dropWhile(_.is_space) match { - case tok1 :: rest1 if tok1.is_text => + case tok1 :: rest1 if tok1.is_embedded => update(rest1, make_comment(tok1) :: result) case _ => update(rest, tok.source :: result) }