Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We鈥檒l occasionally send you account related emails.

Already on GitHub? Sign in to your account

馃捇 Collection of developer tool improvements (mainly editor) #378

Open
7 of 10 tasks
linusha opened this issue May 31, 2022 · 0 comments
Open
7 of 10 tasks

馃捇 Collection of developer tool improvements (mainly editor) #378

linusha opened this issue May 31, 2022 · 0 comments
Assignees

Comments

@linusha
Copy link
Contributor

linusha commented May 31, 2022

This is meant as a collection for various improvements I'd like to get to sometime in the next months.
Feel free to add your own and/or provide feedback/thoughts on the ones listed:

  • Code Folding (e.g. collapse an if block)
  • Line Numbering (see Line numbers聽#42 and Need line numbers in the Object Editor聽#152)
  • Useful Naming of Editor Windows (at least the module name should always be present!)
  • Swap File Support (i.e. save the contents of an text editor every few seconds, without formatting/evaluating it, just to not loose code)
  • TODO and FIXME comments are currently highlighted in the code, this should be done via markers, so that they are displayed on the code map
  • One should be able to open the code map without the search widget~~
  • in general, the text map (with and without search widget) should become a bit more robust. It happens often, that one uses e.g. the scrollbar to scroll in the text and doing so will results in the text map being closed
  • Improve the search widget (i.e. affordable regex and case-(in)sensitive settings)
  • Git Blame (multiline blame) is currently nearly impossible to read, should be improved upon
  • It should never be possible to accidentaly browse in non-focused browsers. The keyboard navigation needs to respect unsaved changes!
@linusha linusha self-assigned this May 31, 2022
@linusha linusha changed the title 馃摦 Collection of developer tool improvements (mainly editor) 馃捇 Collection of developer tool improvements (mainly editor) Jun 2, 2022
This was referenced Oct 19, 2022
@merryman merryman pinned this issue Nov 27, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant