equal
deleted
inserted
replaced
1400 } |
1400 } |
1401 String src = sb.toString(); |
1401 String src = sb.toString(); |
1402 Consumer<String> saveHandler = new SaveHandler(src, srcSet); |
1402 Consumer<String> saveHandler = new SaveHandler(src, srcSet); |
1403 Consumer<String> errorHandler = s -> hard("Edit Error: %s", s); |
1403 Consumer<String> errorHandler = s -> hard("Edit Error: %s", s); |
1404 if (editor == null) { |
1404 if (editor == null) { |
1405 EditPad.edit(errorHandler, src, saveHandler); |
1405 try { |
|
1406 EditPad.edit(errorHandler, src, saveHandler); |
|
1407 } catch (RuntimeException ex) { |
|
1408 errormsg("jshell.err.cant.launch.editor", ex); |
|
1409 fluffmsg("jshell.msg.try.set.editor"); |
|
1410 return false; |
|
1411 } |
1406 } else { |
1412 } else { |
1407 ExternalEditor.edit(editor, errorHandler, src, saveHandler, input); |
1413 ExternalEditor.edit(editor, errorHandler, src, saveHandler, input); |
1408 } |
1414 } |
1409 return true; |
1415 return true; |
1410 } |
1416 } |