73264
|
1 |
(* Title: Pure/System/bash.ML
|
64304
|
2 |
Author: Makarius
|
|
3 |
|
73264
|
4 |
Syntax for GNU bash.
|
64304
|
5 |
*)
|
|
6 |
|
73264
|
7 |
signature BASH =
|
64304
|
8 |
sig
|
|
9 |
val string: string -> string
|
|
10 |
val strings: string list -> string
|
|
11 |
end;
|
|
12 |
|
73264
|
13 |
structure Bash: BASH =
|
64304
|
14 |
struct
|
|
15 |
|
|
16 |
fun string "" = "\"\""
|
|
17 |
| string str =
|
|
18 |
str |> translate_string (fn ch =>
|
|
19 |
let val c = ord ch in
|
|
20 |
(case ch of
|
|
21 |
"\t" => "$'\\t'"
|
|
22 |
| "\n" => "$'\\n'"
|
|
23 |
| "\f" => "$'\\f'"
|
|
24 |
| "\r" => "$'\\r'"
|
|
25 |
| _ =>
|
|
26 |
if Symbol.is_ascii_letter ch orelse Symbol.is_ascii_digit ch orelse
|
67200
|
27 |
exists_string (fn c => c = ch) "+,-./:_" then ch
|
64304
|
28 |
else if c < 16 then "$'\\x0" ^ Int.fmt StringCvt.HEX c ^ "'"
|
|
29 |
else if c < 32 orelse c >= 127 then "$'\\x" ^ Int.fmt StringCvt.HEX c ^ "'"
|
|
30 |
else "\\" ^ ch)
|
|
31 |
end);
|
|
32 |
|
|
33 |
val strings = space_implode " " o map string;
|
|
34 |
|
|
35 |
end;
|