Feature Description:
Currently, with 17667, the "copy" menu will output the problems as a (list of) json objects. It could be convenient to directly export this to a json file. We would like to add the following features as a follow up:
- Add an "export" menu, which will open up a file dialog and write the json object to a user-specified file. When only a header is selected, we might want to export all of its children instead of nothing.
- Add a "copy as text" menu. It shall be similar to copy message, but will also output the file names, which might be more useful than the existing "copy message", since the user would be likely to want to know which file is causing the problem (in addition to the messages themselves), while not necessarily needing all the info in the output of "copy".
- Wire up Ctrl+C and Ctrl+A key bindings for copy (or copy as text, we should discuss) and select all, respectively.
I can open a PR supporting these features, if they sound reasonable. Discussions and suggestions on how they should behave is very appreciated!
Feature Description:
Currently, with 17667, the "copy" menu will output the problems as a (list of) json objects. It could be convenient to directly export this to a json file. We would like to add the following features as a follow up:
I can open a PR supporting these features, if they sound reasonable. Discussions and suggestions on how they should behave is very appreciated!