# HG changeset patch
# User wenzelm
# Date 1515959921 -3600
# Node ID f83c1842a55907c5426611f92fbcfa3b5a9317fb
# Parent  a38c74b0886d54a5402d26887e81784425b60935
trim blanks -- more thoroughly than in update_cartouches (for single-line comments);

diff -r a38c74b0886d -r f83c1842a559 src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Sun Jan 14 20:39:27 2018 +0100
+++ b/src/Pure/General/symbol.scala	Sun Jan 14 20:58:41 2018 +0100
@@ -132,6 +132,9 @@
 
   def length(text: CharSequence): Int = iterator(text).length
 
+  def trim_blanks(text: CharSequence): String =
+    Library.trim(is_blank(_), explode(text)).mkString
+
 
   /* decoding offsets */
 
diff -r a38c74b0886d -r f83c1842a559 src/Pure/Tools/update_comments.scala
--- a/src/Pure/Tools/update_comments.scala	Sun Jan 14 20:39:27 2018 +0100
+++ b/src/Pure/Tools/update_comments.scala	Sun Jan 14 20:58:41 2018 +0100
@@ -20,8 +20,8 @@
         case tok :: rest if tok.source == "--" || tok.source == Symbol.comment =>
           rest.dropWhile(_.is_space) match {
             case tok1 :: rest1 if tok1.is_text =>
-              val res = Symbol.comment + Symbol.space + Library.cartouche(tok1.content)
-              update(rest1, res :: result)
+              val txt = Symbol.trim_blanks(tok1.content)
+              update(rest1, (Symbol.comment + Symbol.space + Library.cartouche(txt)) :: result)
             case _ => update(rest, tok.source :: result)
           }
         case tok :: rest => update(rest, tok.source :: result)