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.

Sign up for GitHub

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

Jump to bottom

Term selection and reference highlighting on different sequents. #167

Open
SpringVaS opened this issue Apr 22, 2020 · 3 comments
Open

Term selection and reference highlighting on different sequents. #167

SpringVaS opened this issue Apr 22, 2020 · 3 comments
Assignees
@SpringVaS

Comments

@SpringVaS
Copy link
Collaborator

Term selection and reference highlighting in the displayed sequent is stored in a way that it is applied on any sequent that is selected. Also the reference highlighting in the editor is not cleared. This leads to inconsistent displays.
InconsistentRefHigh
@SpringVaS SpringVaS changed the title Term selection and reference highlighting stored "globally". Term selection and reference highlighting on different sequents. Apr 22, 2020
@SpringVaS SpringVaS self-assigned this Apr 22, 2020
@JonasKlamroth
Copy link
Collaborator

@SpringVaS can you check whether or not not #188 is resolving this?

@SpringVaS
Copy link
Collaborator Author

Unfortunately, it does not.
issue

@SpringVaS
Copy link
Collaborator Author

Furthermore, the variable is sometimes highlighted at the wrong position. As in the following picture.
nissue

JonasKlamroth added a commit that referenced this issue Aug 28, 2020
@JonasKlamroth
improved reference highlight handling:
78d944e 
- editor view is shown when reference highlighting is requested
- automatic scrolling to first highlighted reference
- selecting a different pvc now resets the reference highlighted term (towards #167)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@SpringVaS SpringVaS

Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@JonasKlamroth @SpringVaS