Revert "Fix CurrentGoalView highlights not being removed"

[mattulbrich]

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

• Bug fix (non-breaking change which fixes an issue)

Ensuring quality

• I have tested the feature as follows: Tried it in the gui

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

[codecov[bot]]

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

@@            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]

@unp1 Might be connected to your PR.

[mattulbrich]

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]

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]

@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]

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

@wadoon How do I remerge this PR now?