# HG changeset patch # User wenzelm # Date 1459795554 -7200 # Node ID d8cf59edf819bcadb54b0df191871bcb1ff4822d # Parent 8e54fd480809dd17443efeb9c528045cde2e33d9 allow empty string; diff -r 8e54fd480809 -r d8cf59edf819 src/Pure/General/file.ML --- 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; diff -r 8e54fd480809 -r d8cf59edf819 src/Pure/General/file.scala --- 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(" ")