| 412 | } |
| 413 | |
| 414 | public void keyReleased(KeyEvent e) { |
| 415 | if (e.getSource() == pageCanvas) { |
| 416 | int c = e.getKeyCode(); |
| 417 | |
| 418 | switch(c) |
| 419 | { |
| 420 | case KeyEvent.VK_F1: showHelp(); break; |
| 421 | |
| 422 | case KeyEvent.VK_LEFT: pan(-10, 0); break; |
| 423 | case KeyEvent.VK_RIGHT: pan(+10, 0); break; |
| 424 | case KeyEvent.VK_UP: pan(0, -10); break; |
| 425 | case KeyEvent.VK_DOWN: pan(0, +10); break; |
| 426 | |
| 427 | case KeyEvent.VK_PAGE_UP: doc.flipPages(-number, null); break; |
| 428 | case KeyEvent.VK_PAGE_DOWN: doc.flipPages(+number, null); break; |
| 429 | } |
| 430 | } |
| 431 | } |
| 432 | |
| 433 | public void keyTyped(KeyEvent e) { |
| 434 | if (e.getSource() == pageCanvas) |