Abbreviations Manager

[wadoon]

Abbreviations are built-in to the KeY system, but this construct is not very popular. This may be to their volatility: you are not able to store, and reuse them on new proof attempts.
This PR brings a new widget:

The widget offers following features:

• view current defined abbreviations
• load and store abbreviation mappings
  • A text file where each line <label>::==<term> describes an abbreviation.
• transfer (import) abbreviations of currently open proofs
• Context menu:
  • change the abbreviation label
  • delete an abbreviation
  • disable an abbreviate

[codecov]

Codecov Report

Attention: 57 lines in your changes are missing coverage. Please review.

Comparison is base (603b2ca) 37.93% compared to head (ee98653) 37.97%.

❗ Current head ee98653 differs from pull request most recent head 6a80690. Consider uploading reports for the commit 6a80690 to get more accurate results

Files	Patch %	Lines
...re/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java	14.58%	41 Missing ⚠️
...ain/java/org/key_project/util/java/StringUtil.java	0.00%	16 Missing ⚠️

Additional details and impacted files

@@             Coverage Diff              @@
##               main    #3202      +/-   ##
============================================
+ Coverage     37.93%   37.97%   +0.04%     
+ Complexity    17030    17024       -6     
============================================
  Files          2060     2059       -1     
  Lines        126300   126060     -240     
  Branches      21304    21280      -24     
============================================
- Hits          47913    47874      -39     
+ Misses        72499    72304     -195     
+ Partials       5888     5882       -6     

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

[github-actions]

Thank you for your contribution.

The test artifacts are available on Artiweb.
The newest artifact is here.

[jwiesler]

Thanks for abbreviation delete!

What would be great imo is if I try to create an abbreviation and that name is already taken: Show an option to remove the old and use this as the new label term.

[jwiesler]

Can't this be stored in the proof file itself? I think this would be a better place to store.

[wadoon]

Can't this be stored in the proof file itself? I think this would be a better place to store.

My current story for load/store is that you attempt to proof something, notice a specification (or KeY) failure, fix it and restart the attempt. Then you can rescue the abbreviations.

Proof attempts are rather not stored as proof files. But maybe we should consider storing the abbreviations in the settings. I would wait for #3031 for a type-safe lists in the settings.

[jwiesler]

#3031 is already merged?

Settings would be a good idea as well.

[wadoon]

#3031 is already merged?

Settings would be a good idea as well.

Sorry, mean #3099

[FliegendeWurst]

I am confused by the save abbreviations dialog. It suggests to save this data as a .proof:

p::==i_arr_5
d::==i_arr_2
l::==i_arr_8

[FliegendeWurst]

How does the load abbreviations functionality work? I selected my previously saved file, but no abbreviations were restored.

[FliegendeWurst]

The abbreviations transfer does not work for program variables. I think they would need to be compared by name, not by identity.