equal
deleted
inserted
replaced
11 BufferedWriter, OutputStreamWriter} |
11 BufferedWriter, OutputStreamWriter} |
12 |
12 |
13 |
13 |
14 object Bash |
14 object Bash |
15 { |
15 { |
|
16 /* concrete syntax */ |
|
17 |
|
18 private def bash_chr(c: Byte): String = |
|
19 { |
|
20 val ch = c.toChar |
|
21 ch match { |
|
22 case '\t' => "$'\\t'" |
|
23 case '\n' => "$'\\n'" |
|
24 case '\f' => "$'\\f'" |
|
25 case '\r' => "$'\\r'" |
|
26 case _ => |
|
27 if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch)) |
|
28 Symbol.ascii(ch) |
|
29 else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" |
|
30 else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" |
|
31 else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'" |
|
32 else "\\" + ch |
|
33 } |
|
34 } |
|
35 |
|
36 def string(s: String): String = |
|
37 if (s == "") "\"\"" |
|
38 else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString |
|
39 |
|
40 def strings(ss: List[String]): String = |
|
41 ss.iterator.map(Bash.string(_)).mkString(" ") |
|
42 |
|
43 |
|
44 /* process and result */ |
|
45 |
16 private class Limited_Progress(proc: Process, progress_limit: Option[Long]) |
46 private class Limited_Progress(proc: Process, progress_limit: Option[Long]) |
17 { |
47 { |
18 private var count = 0L |
48 private var count = 0L |
19 def apply(progress: String => Unit)(line: String): Unit = synchronized { |
49 def apply(progress: String => Unit)(line: String): Unit = synchronized { |
20 progress(line) |
50 progress(line) |