static void print_doubleNL(O o) {
  print("\n" + str(o) + "\n");
}