# HG changeset patch # User wenzelm # Date 1484578254 -3600 # Node ID 14c760e0e1cffe012833d3e8978874abd5c8d81d # Parent ba72a13eb78c507995797ce135fefb504bcb0242 tuned -- nicer generated bash source; diff -r ba72a13eb78c -r 14c760e0e1cf src/Pure/System/bash.scala --- a/src/Pure/System/bash.scala Sun Jan 15 16:47:42 2017 +0100 +++ b/src/Pure/System/bash.scala Mon Jan 16 15:50:54 2017 +0100 @@ -24,7 +24,7 @@ case '\f' => "$'\\f'" case '\r' => "$'\\r'" case _ => - if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch)) + if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+-./:_".contains(ch)) Symbol.ascii(ch) else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" diff -r ba72a13eb78c -r 14c760e0e1cf src/Pure/System/bash_syntax.ML --- a/src/Pure/System/bash_syntax.ML Sun Jan 15 16:47:42 2017 +0100 +++ b/src/Pure/System/bash_syntax.ML Mon Jan 16 15:50:54 2017 +0100 @@ -24,7 +24,7 @@ | "\r" => "$'\\r'" | _ => if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse - exists_string (fn c => c = ch) "-./:_" then ch + 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)