+ public static final class Redirect extends JSElement {
+ public Redirect(XML.Element e) { super(e); }
+
+ public void out(Writer w) throws IOException {
+ loadAttr();
+
+ try {
+ Object p = get("page"); if (p != null) undeclare("page");
+ if (p == null || !(p instanceof String) || ((String)p).trim().equals(""))
+ throw new JSElement.Exn("<"+getPrefix()+":redirect> requires 'page' "+
+ "attribute to be a valid template path");
+ throw new RedirectSignal((String)p);
+ } catch (JSExn e) { throw new JSElement.Exn(e); }
+ }
+ }
+