diff -r 3e001fe6f16a -r 29ca4cdd998d src/Pure/Tools/check_sources.scala
--- a/src/Pure/Tools/check_sources.scala	Sat Apr 02 15:06:41 2016 +0200
+++ b/src/Pure/Tools/check_sources.scala	Sat Apr 02 15:40:06 2016 +0200
@@ -28,7 +28,7 @@
             Position.here(line_pos(i)))
         }
       }
-      catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
+      catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
 
       if (line.contains('\t'))
         Output.warning("TAB character" + Position.here(line_pos(i)))
@@ -36,6 +36,9 @@
 
     if (content.contains('\r'))
       Output.warning("CR character" + Position.here(file_pos))
+
+    if (Word.bidi_detect(content))
+      Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
   }
 
   def check_hg(root: Path)