}
public Date datetime() {
if (type != QUOTED) bad("Expected quoted datetime");
- try { return new SimpleDateFormat("dd-MM-yyyy hh:mm:ss zzzz").parse(s.trim());
+ try { return new SimpleDateFormat("dd-MMM-yyyy hh:mm:ss zzzz").parse(s.trim());
} catch (ParseException p) { throw new Server.Bad("invalid datetime format " + s + " : " + p); }
}
public String atom() {
")";
}
+ // FIXME: ugly
+ public static String qq(Stream stream) {
+ StringBuffer sb = new StringBuffer();
+ stream.transcribe(sb);
+ return sb.toString();
+ }
public static String qq(String s) {
StringBuffer ret = new StringBuffer();
ret.append('{');