equal
deleted
inserted
replaced
106 def shell_quote(s: String): String = "'" + s + "'" |
106 def shell_quote(s: String): String = "'" + s + "'" |
107 def shell_path(path: Path): String = shell_quote(standard_path(path)) |
107 def shell_path(path: Path): String = shell_quote(standard_path(path)) |
108 def shell_path(file: JFile): String = shell_quote(standard_path(file)) |
108 def shell_path(file: JFile): String = shell_quote(standard_path(file)) |
109 |
109 |
110 |
110 |
|
111 /* directory entries */ |
|
112 |
|
113 def check_dir(path: Path): Path = |
|
114 if (path.is_dir) path else error("No such directory: " + path) |
|
115 |
|
116 def check_file(path: Path): Path = |
|
117 if (path.is_file) path else error("No such file: " + path) |
|
118 |
|
119 |
111 /* find files */ |
120 /* find files */ |
112 |
121 |
113 def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] = |
122 def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] = |
114 { |
123 { |
115 val result = new mutable.ListBuffer[JFile] |
124 val result = new mutable.ListBuffer[JFile] |