recode utf8 for ML, as done in feeder.pl;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/scripts/recode.pl	Thu Aug 01 22:20:07 2013 +0200
@@ -0,0 +1,12 @@
+#
+# Author: Makarius
+#
+# recode.pl - recode utf8 for ML
+#
+
+for (@ARGV) {
+  utf8::upgrade($_);
+  s/([\x80-\xff])/\\${\(ord($1))}/g;
+  print $_, " ";
+}
+

--- a/lib/scripts/run-polyml-5.5.1	Thu Aug 01 22:19:32 2013 +0200
+++ b/lib/scripts/run-polyml-5.5.1	Thu Aug 01 22:20:07 2013 +0200
@@ -64,7 +64,8 @@
 MLTEXT="$INIT $EXIT $COMMIT $MLTEXT"
 
 if [ -n "$TERMINATE" -a -z "$MLEXIT" ]; then
-  "$POLY" -q -i $ML_OPTIONS --eval "$MLTEXT" --error-exit </dev/null
+  "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" \
+    --error-exit </dev/null
   RC="$?"
 else
   if [ -z "$TERMINATE" ]; then