equal
deleted
inserted
replaced
139 |
139 |
140 def check_file(path: Path): Path = |
140 def check_file(path: Path): Path = |
141 if (path.is_file) path else error("No such file: " + path) |
141 if (path.is_file) path else error("No such file: " + path) |
142 |
142 |
143 |
143 |
144 /* find files */ |
144 /* directory content */ |
|
145 |
|
146 def read_dir(dir: Path): List[String] = |
|
147 { |
|
148 if (!dir.is_dir) error("Bad directory: " + dir.toString) |
|
149 val files = dir.file.listFiles |
|
150 if (files == null) Nil |
|
151 else files.toList.map(_.getName) |
|
152 } |
145 |
153 |
146 def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] = |
154 def find_files(start: JFile, pred: JFile => Boolean = _ => true): List[JFile] = |
147 { |
155 { |
148 val result = new mutable.ListBuffer[JFile] |
156 val result = new mutable.ListBuffer[JFile] |
149 |
157 |