equal
deleted
inserted
replaced
41 def is_wellformed(name: String): Boolean = |
41 def is_wellformed(name: String): Boolean = |
42 try { Url(name); true } |
42 try { Url(name); true } |
43 catch { case ERROR(_) => false } |
43 catch { case ERROR(_) => false } |
44 |
44 |
45 def is_readable(name: String): Boolean = |
45 def is_readable(name: String): Boolean = |
46 try { Url(name).openStream.close; true } |
46 try { Url(name).openStream.close(); true } |
47 catch { case ERROR(_) => false } |
47 catch { case ERROR(_) => false } |
48 |
48 |
49 |
49 |
50 /* trim index */ |
50 /* trim index */ |
51 |
51 |