--- a/src/Pure/Admin/check_sources.scala Tue Dec 20 08:46:38 2016 +0100
+++ b/src/Pure/Admin/check_sources.scala Tue Dec 20 08:53:26 2016 +0100
@@ -25,9 +25,9 @@
try {
Symbol.decode_strict(line)
- for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+ for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
{
- Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+ Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
Position.here(line_pos(i)))
}
}