--- a/src/Pure/General/file.ML Mon Apr 04 20:28:17 2016 +0200
+++ b/src/Pure/General/file.ML Mon Apr 04 20:45:54 2016 +0200
@@ -46,21 +46,22 @@
val standard_path = Path.implode o Path.expand;
val platform_path = ML_System.platform_path o standard_path;
-val bash_string =
- translate_string (fn ch =>
- let val c = ord ch in
- (case ch of
- "\t" => "$'\\t'"
- | "\n" => "$'\\n'"
- | "\f" => "$'\\f'"
- | "\r" => "$'\\r'"
- | _ =>
- if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
- exists_string (fn c => c = ch) "-./:_" then ch
- else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
- else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
- else "\\" ^ ch)
- end);
+fun bash_string "" = "\"\""
+ | bash_string str =
+ str |> translate_string (fn ch =>
+ let val c = ord ch in
+ (case ch of
+ "\t" => "$'\\t'"
+ | "\n" => "$'\\n'"
+ | "\f" => "$'\\f'"
+ | "\r" => "$'\\r'"
+ | _ =>
+ if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
+ exists_string (fn c => c = ch) "-./:_" then ch
+ else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
+ else "\\" ^ ch)
+ end);
val bash_args = space_implode " " o map bash_string;
--- a/src/Pure/General/file.scala Mon Apr 04 20:28:17 2016 +0200
+++ b/src/Pure/General/file.scala Mon Apr 04 20:45:54 2016 +0200
@@ -123,7 +123,8 @@
}
def bash_string(s: String): String =
- UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
+ if (s == "") "\"\""
+ else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
def bash_args(args: List[String]): String =
args.iterator.map(bash_string(_)).mkString(" ")