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)
           }