()
| 1416 | } |
| 1417 | |
| 1418 | protected void revert() { |
| 1419 | if (!changes) |
| 1420 | return; |
| 1421 | String title = getTitle(); |
| 1422 | if (path==null || !(new File(path).exists()) || !path.endsWith(title)) { |
| 1423 | IJ.showStatus("Cannot revert, no file "+getTitle()); |
| 1424 | return; |
| 1425 | } |
| 1426 | if (!IJ.showMessageWithCancel("Revert?", "Revert to saved version of\n\""+getTitle()+"\"?")) |
| 1427 | return; |
| 1428 | String directory = path.substring(0, path.length()-title.length()); |
| 1429 | open(directory, title); |
| 1430 | undoBuffer = new ArrayList(); |
| 1431 | } |
| 1432 | |
| 1433 | /** Changes a plugins class name to reflect a new file name. */ |
| 1434 | public void updateClassName(String oldName, String newName) { |
no test coverage detected