Add commentstring setting.

The commentstring setting is used in plugins like Tim Pope's
"commentary" plugin.  commentstring defaults to "/*", which is not
usable by idris.  This commit changes it to "--".
Merge pull request #28 from cdepillabout/add-commentstring-setting

Add commentstring setting.