# HG changeset patch
# User wenzelm
# Date 1457379887 -3600
# Node ID f8ebb715e06d3a77a19b232a1b72eacec695b84a
# Parent  b33dea50366597401ff2363b697f897ac52038c5
clarified treatment of DEL;
tuned signature;

diff -r b33dea503665 -r f8ebb715e06d src/Pure/General/file.scala
--- a/src/Pure/General/file.scala	Mon Mar 07 18:47:55 2016 +0100
+++ b/src/Pure/General/file.scala	Mon Mar 07 20:44:47 2016 +0100
@@ -103,7 +103,7 @@
 
   /* bash path */
 
-  private def bash_escape(c: Byte): String =
+  private def bash_chr(c: Byte): String =
   {
     val ch = c.toChar
     ch match {
@@ -116,19 +116,19 @@
           Symbol.ascii(ch)
         else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
         else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
-        else if (c < 32) "$'\\x" + Integer.toHexString(c) + "'"
+        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
         else  "\\" + ch
     }
   }
 
-  def bash_escape(s: String): String =
-    UTF8.bytes(s).iterator.map(bash_escape(_)).mkString
+  def bash_string(s: String): String =
+    UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
 
-  def bash_escape(args: List[String]): String =
-    args.iterator.map(bash_escape(_)).mkString(" ")
+  def bash_args(args: List[String]): String =
+    args.iterator.map(bash_string(_)).mkString(" ")
 
-  def bash_path(path: Path): String = bash_escape(standard_path(path))
-  def bash_path(file: JFile): String = bash_escape(standard_path(file))
+  def bash_path(path: Path): String = bash_string(standard_path(path))
+  def bash_path(file: JFile): String = bash_string(standard_path(file))
 
 
   /* directory entries */
diff -r b33dea503665 -r f8ebb715e06d src/Pure/System/isabelle_process.scala
--- a/src/Pure/System/isabelle_process.scala	Mon Mar 07 18:47:55 2016 +0100
+++ b/src/Pure/System/isabelle_process.scala	Mon Mar 07 20:44:47 2016 +0100
@@ -17,8 +17,8 @@
     val system_process =
       try {
         val process =
-          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_escape(system_channel.server_name) +
-            " " + File.bash_escape(prover_args))
+          Bash.process("\"$ISABELLE_PROCESS\" -P " + File.bash_string(system_channel.server_name) +
+            " " + File.bash_args(prover_args))
         process.stdin.close
         process
       }
diff -r b33dea503665 -r f8ebb715e06d src/Pure/System/ml_process.scala
--- a/src/Pure/System/ml_process.scala	Mon Mar 07 18:47:55 2016 +0100
+++ b/src/Pure/System/ml_process.scala	Mon Mar 07 20:44:47 2016 +0100
@@ -88,7 +88,7 @@
         chmod $(umask -S) "$ISABELLE_TMP"
 
         librarypath "$ML_HOME"
-        "$ML_HOME/poly" -q -i """ + File.bash_escape(bash_args) + """
+        "$ML_HOME/poly" -q -i """ + File.bash_args(bash_args) + """
         RC="$?"
 
         rm -f "$ISABELLE_PROCESS_OPTIONS"