# HG changeset patch
# User wenzelm
# Date 1459604406 -7200
# Node ID 29ca4cdd998d47a4dbcd25723c044a388e68af6b
# Parent  3e001fe6f16ae16192ea61922333d0debf9eef89
clarified check_sources;

diff -r 3e001fe6f16a -r 29ca4cdd998d Admin/lib/Tools/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 "$@"
diff -r 3e001fe6f16a -r 29ca4cdd998d lib/Tools/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 "$@"
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)