| 448 | String ZEROS = "000"; |
| 449 | |
| 450 | private void acceptLine( String line ) |
| 451 | { |
| 452 | // Patch to handle Unicode characters |
| 453 | // Submitted by Daniel Leuck |
| 454 | StringBuilder buf = new StringBuilder(); |
| 455 | int lineLength = line.length(); |
| 456 | for(int i=0; i<lineLength; i++) { |
| 457 | String val = Integer.toString(line.charAt(i), 16); |
| 458 | val=ZEROS.substring(0,4-val.length()) + val; |
| 459 | buf.append("\\u" + val); |
| 460 | } |
| 461 | line = buf.toString(); |
| 462 | // End unicode patch |
| 463 | |
| 464 | if (outPipe == null ) |
| 465 | print("Console internal error: cannot output ...", Color.red); |
| 466 | else |
| 467 | try { |
| 468 | outPipe.write( line.getBytes() ); |
| 469 | outPipe.flush(); |
| 470 | } catch ( IOException e ) { |
| 471 | outPipe = null; |
| 472 | throw new RuntimeException("Console pipe broken..."); |
| 473 | } |
| 474 | //text.repaint(); |
| 475 | } |
| 476 | |
| 477 | public void println(Object o) { |
| 478 | print( String.valueOf(o) + "\n" ); |