jshell tool: external editor temp file should be *.java

Generated file should end in ".java" for editors (like jEdit) which key formatting off the filename extension.