(boolean larger)
| 401 | } |
| 402 | |
| 403 | void changeFontSize(boolean larger) { |
| 404 | int in = fontSize; |
| 405 | if (larger) { |
| 406 | fontSize++; |
| 407 | if (fontSize==sizes.length) |
| 408 | fontSize = sizes.length-1; |
| 409 | } else { |
| 410 | fontSize--; |
| 411 | if (fontSize<0) |
| 412 | fontSize = 0; |
| 413 | } |
| 414 | IJ.showStatus(sizes[fontSize]+" point"); |
| 415 | font = null; |
| 416 | setFont(); |
| 417 | } |
| 418 | |
| 419 | public static void setFont(String name, int style, int size) { |
| 420 | font = new Font(name,style,size); |
no test coverage detected