Reverse Origin Lookup

[unp1]

Please describe your proposal in a ONE sentence

One sentence describing your idea

Selection of a JML line in the source view leads to highlighting all formulas of that origin in the sequent view

Underlying problem

A clear and concise description of what the problem is. Ex. I'm always frustrated when [...]

Comprehension of the encountered proof situation requires to map JML specifications to DL formulas. We have one direction (from DL to JML), this feature request suggests to support the reverse direction.

Usage Scenario

Who (user scenario) would benefit from implementing the idea?
Describe a short use case scenario in which the suggested idea is featured.
Describe the solution you'd like: A clear and concise description of what you want to happen.

For understanding a complex proof situation, it would be helpful to identify all formulas in the sequent relating to a JML expression.
For example, when performing a proof containing a loop it is useful to identify the relevant (often the same part one is currently proving) assumed part of a loop invariant

Alternatives

A clear and concise description of any alternative solutions or features you've considered.
Why is the suggestion the best alternative?

none evaluated

Estimated effort

If you can: Estimate the effort that has to be invested to implement the feature request.
Is there still discussion needed? Or is it purely implementation? Expertises needed?

I don't know. As we have already one direction, the reverse seems to be more like a search through the sequent and looking at term labels.

Additional context

Add any other context or screenshots about the feature request here.

[WolframPfeifer]

There is the work of a master's student who implemented something similar. I have to look if this can be merged to main (larger amount of work, therefore postponed after the HacKeYthon).