search

KeYProject / key

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

`TermLabelVisibilityManager` only receivable via MainWindow, which creates a window. #3131

Open wadoon opened 1 year ago

wadoon commented 1 year ago

Using KeY as a library is not possible, if MainWindow is accessed.

Scenario:

I need pretty printing of KeY formulas in an external program. For this I want require a TermLabelVisibilityManager which I can only get via MainWindow. Calling MainWindow#getInstance() opens the window.

Closing this closes KeY! Also not good.

This blocks the usage of KeY as a library :exclamation:

jwiesler commented 1 year ago

I don't understand. TermLabelVisibilityManager has a constructor with 0 arguments (which is even used inside LogicPrinter) and is in key.core, so it can not depend on MainWindow.

Furthermore, the printers accept the interface VisibleTermLabels, so there isn't even a need for a TermLabelVisibilityManager.