tuned;

--- a/src/Pure/General/word.scala	Tue Apr 29 16:14:27 2014 +0200
+++ b/src/Pure/General/word.scala	Tue Apr 29 20:40:44 2014 +0200
@@ -27,6 +27,8 @@
       }
     }
 
+  def codepoint(c: Int): String = new String(Array(c), 0, 1)
+
 
   /* case */
 

--- a/src/Pure/Tools/check_source.scala	Tue Apr 29 16:14:27 2014 +0200
+++ b/src/Pure/Tools/check_source.scala	Tue Apr 29 20:40:44 2014 +0200
@@ -24,18 +24,18 @@
 
         for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
         {
-          Output.warning("Suspicious Unicode character " + quote(new String(Array(c), 0, 1)) +
+          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
             Position.here(line_pos(i)))
         }
       }
       catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
 
       if (line.contains('\t'))
-        Output.warning("TAB character " + Position.here(line_pos(i)))
+        Output.warning("TAB character" + Position.here(line_pos(i)))
     }
 
     if (content.contains('\r'))
-      Output.warning("CR character " + Position.here(file_pos))
+      Output.warning("CR character" + Position.here(file_pos))
   }
 }