equal
deleted
inserted
replaced
57 |
57 |
58 geometry |
58 geometry |
59 } |
59 } |
60 |
60 |
61 |
61 |
62 /* files */ |
62 /* plain files */ |
63 |
63 |
64 def is_file(name: String): Boolean = |
64 def is_file(name: String): Boolean = |
65 VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] |
65 name != null && name.nonEmpty && VFSManager.getVFSForPath(name).isInstanceOf[FileVFS] |
66 |
66 |
67 def check_file(name: String): Option[JFile] = |
67 def check_file(name: String): Option[JFile] = |
68 if (is_file(name)) Some(new JFile(name)) else None |
68 if (is_file(name)) Some(new JFile(name)) else None |
69 |
69 |
70 |
70 |