# HG changeset patch
# User wenzelm
# Date 1398796844 -7200
# Node ID 792dd0e9cebb63ca6561b5cb38d7842f3250bb83
# Parent  23883e1879c5ddcb7d26482ce56b7f46a09dbe03
tuned;

diff -r 23883e1879c5 -r 792dd0e9cebb src/Pure/General/word.scala
--- 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 */
 
diff -r 23883e1879c5 -r 792dd0e9cebb src/Pure/Tools/check_source.scala
--- 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))
   }
 }