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’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Expand source editor visible range #41

ktraunmueller opened this issue Jul 4, 2017 · 1 comment


1 participant
Copy link

commented Jul 4, 2017

Expand the range of source shown in the source editor beyond the current paragraph (also show stuff preceding and following the current scope).

This should help as a fallback with missing source info in section headers, etc. E.g., the CRing section headers ("§1 Introduction") have no source info, and this would help a lot there.


  • maybe show "go to previous / next scope" arrows instead of showing more source in the editor?
  • maybe add an "expand editor range" button?

@ktraunmueller ktraunmueller added this to the 1.0 milestone Jul 4, 2017

@ktraunmueller ktraunmueller modified the milestones: 1.0, 1.2 Jan 4, 2018

@ktraunmueller ktraunmueller modified the milestones: 1.2, Not yet scheduled Feb 14, 2018

@ktraunmueller ktraunmueller self-assigned this Mar 19, 2019

@ktraunmueller ktraunmueller changed the title Expand source editor range Expand source editor visible range Mar 19, 2019

@ktraunmueller ktraunmueller removed their assignment Mar 20, 2019


This comment has been minimized.

Copy link
Owner Author

commented Mar 20, 2019

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.