99 else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') |
99 else if (s.startsWith("\\\\")) "file:" + s.replace('\\', '/') |
100 else "file:///" + s.replace('\\', '/') |
100 else "file:///" + s.replace('\\', '/') |
101 } |
101 } |
102 |
102 |
103 |
103 |
104 /* shell path (bash) */ |
104 /* bash path */ |
105 |
105 |
106 def shell_quote(s: String): String = "'" + s + "'" |
106 private def bash_escape(c: Byte): String = |
107 def shell_path(path: Path): String = shell_quote(standard_path(path)) |
107 { |
108 def shell_path(file: JFile): String = shell_quote(standard_path(file)) |
108 val ch = c.toChar |
|
109 ch match { |
|
110 case '\t' => "$'\\t'" |
|
111 case '\n' => "$'\\n'" |
|
112 case '\f' => "$'\\f'" |
|
113 case '\r' => "$'\\r'" |
|
114 case _ => |
|
115 if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "-./:_".contains(ch)) |
|
116 Symbol.ascii(ch) |
|
117 else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'" |
|
118 else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'" |
|
119 else if (c < 32) "$'\\x" + Integer.toHexString(c) + "'" |
|
120 else "\\" + ch |
|
121 } |
|
122 } |
|
123 |
|
124 def bash_escape(s: String): String = |
|
125 UTF8.bytes(s).iterator.map(bash_escape(_)).mkString |
|
126 |
|
127 def bash_escape(args: List[String]): String = |
|
128 args.iterator.map(bash_escape(_)).mkString(" ") |
|
129 |
|
130 def bash_path(path: Path): String = bash_escape(standard_path(path)) |
|
131 def bash_path(file: JFile): String = bash_escape(standard_path(file)) |
109 |
132 |
110 |
133 |
111 /* directory entries */ |
134 /* directory entries */ |
112 |
135 |
113 def check_dir(path: Path): Path = |
136 def check_dir(path: Path): Path = |