# HG changeset patch # User wenzelm # Date 1516090336 -3600 # Node ID f075640b8868ce85f703bc17df1fc5129d93111d # Parent cafbb63f10e57d42898e6f7802c09b3d9c7eeb11 uniform treatment of old-style and new-style comments; diff -r cafbb63f10e5 -r f075640b8868 src/Pure/Tools/update_comments.scala --- a/src/Pure/Tools/update_comments.scala Tue Jan 16 09:08:06 2018 +0100 +++ b/src/Pure/Tools/update_comments.scala Tue Jan 16 09:12:16 2018 +0100 @@ -14,16 +14,21 @@ { def update_comments(path: Path) { + def make_comment(tok: Token): String = + Symbol.comment + Symbol.space + Symbol.cartouche(Symbol.trim_blanks(tok.content)) + @tailrec def update(toks: List[Token], result: List[String]): String = { toks match { - case tok :: rest if tok.source == "--" || tok.source == Symbol.comment => + case tok :: rest + if tok.source == "--" || tok.source == Symbol.comment => rest.dropWhile(_.is_space) match { case tok1 :: rest1 if tok1.is_text => - val txt = Symbol.trim_blanks(tok1.content) - update(rest1, (Symbol.comment + Symbol.space + Symbol.cartouche(txt)) :: result) + update(rest1, make_comment(tok1) :: result) case _ => update(rest, tok.source :: result) } + case tok :: rest if tok.is_formal_comment && tok.source.startsWith(Symbol.comment) => + update(rest, make_comment(tok) :: result) case tok :: rest => update(rest, tok.source :: result) case Nil => result.reverse.mkString }