It would be great, if a download-function could be integrated into the plugin as it is used with this plugin for example: http://wordpress.org/extend/plugins/wp-syntax-download-extension
The admin defines a filename and if the user clicks on download, a new file gets created with this filename which can be saved.
This saves the now necessary steps "copying to clipboard", open notepad, pasting text, saving as new file, exit.