unp1

Ask before closing a proof whose branches are "used" in other proofs

1

## Please describe your proposal in a ONE sentence Removing a proof might unexpectedly reopen branches on other proofs ## Underlying problem Removing a proof that is referred to by...

## Please describe your proposal in a ONE sentence If the proof tree view is not visible the GUI proof tree should not be updated. ## Underlying problem Updating the...

## Description > Please describe your concern in detail! The SourceView seems not too highlight symbolically executed statements in green, if the contract to be proven is inherited. ## Reproducible...

Reverse Origin Lookup

1

## 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...

Fix for the LoopInvariantConfigurationDialog

9

## Related Issue This PR fixes a bug that prevented the interactive provision of a loop invariant. ## Intended Change It should be possible to enter loop invariants manually. ##...

## Please describe your proposal in a ONE sentence Allow rulesets (heuristics) to be defined with a list of additional arguments ## Underlying problem For several rulesets the strategies have...

Node selection after loading a proof

4

## Description Loading an open proof selects the root node instead of an open goal. I am not sure if that may be intended behavior, because one can be of...

KeY GUI slows down already at proofs of size 10000

1

## Description The proof tree rendering slows down for medium sized proof trees. ## Reproducible always ### Steps to reproduce > What is your expected behavior and what was the...

Remove sequent formula

1

## Intended Change This PR prepares the ground for generalizing proof and calculus structures. It removes the superfluous SequentFormula class, which is only a behaviorless container for a term. The...