clarified check_sources;

--- a/Admin/lib/Tools/check_sources	Sat Apr 02 15:06:41 2016 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-#!/usr/bin/env bash
-#
-# Author: Makarius
-#
-# DESCRIPTION: some sanity checks for Isabelle sources
-
-isabelle_admin_build jars || exit $?
-
-isabelle java isabelle.Check_Sources "$@"

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/Tools/check_sources	Sat Apr 02 15:40:06 2016 +0200
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: some sanity checks for Isabelle sources
+
+isabelle_admin_build jars || exit $?
+
+isabelle java isabelle.Check_Sources "$@"

--- 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)