+
+ /** returns an InputStream containing the Resource's contents */
+ public InputStream getInputStream() throws IOException { return getInputStream(""); }
+ public abstract InputStream getInputStream(String path) throws IOException;
+
+ /** graft newResource in place of this resource on its parent */
+ public Res graft(Object newResource) { throw new JS.Exn("cannot graft onto this resource"); }
+
+ /** if the path of this resource does not end with extension, return a new one wit it appended */
+ public Res addExtension(String extension) { return new Ref(this, extension); }
+
+ public Object[] keys() { throw new JS.Exn("cannot enumerate a resource"); }
+ public void put(Object key, Object val) { throw new JS.Exn("cannot put to a resource"); }