search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
41 stars 24 forks source link

Revert "Fix CurrentGoalView highlights not being removed" #3391

Closed mattulbrich closed 2 weeks ago

mattulbrich commented 7 months ago

Related Issue

This pull request addresses #3378.

Intended Change

This reverts commit 4759370f719ed506746e7a2a13832eac48cfc6c1.

As discussed during a developers meeting, the highlighting is quite important during drag'n'drop.

It reenables the highlighter when drag-n-dropping terms. Moreover, it repairs heatmap toggling.

Type of pull request

Ensuring quality

The contributions within this pull request are licensed under GPLv2 (only) for inclusion in KeY.

codecov[bot] commented 7 months ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 38.16%. Comparing base (0ebb8b5) to head (0df9c3c). Report is 25 commits behind head on main.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #3391 +/- ## ========================================= Coverage 38.16% 38.16% Complexity 17222 17222 ========================================= Files 2109 2109 Lines 127643 127643 Branches 21458 21458 ========================================= Hits 48710 48710 Misses 72943 72943 Partials 5990 5990 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.

WolframPfeifer commented 6 months ago

@unp1 Might be connected to your PR.

mattulbrich commented 1 month ago

The drag'n'drop highlights work now, but unfortunately it breaks other things: Toggling the heat maps does not work anymore, it is necessary to apply/remove a rule to trigger the repaint.

Toggling heat maps does not work on main either. That is a different problem. This is not the problem of this change ... But I will look into this anyway.

mattulbrich commented 1 month ago

Moreover, on main, if the formula is a single line, then mouse highlighting does not work, too. Again, nothing to do with this change.

WolframPfeifer commented 3 weeks ago

@mattulbrich Do you have a good idea how to fix the problem with the non-goal views? If so, could you update it, please? If not, feel free to merge. The remaining UI bug is minor.

mattulbrich commented 2 weeks ago

I have worked on this. Is this fixed now, @WolframPfeifer ?

@wadoon How do I remerge this PR now?