Feature/#1364 debug group should not be shown #2132
Merged
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Updated DefaultProofExplanationTextPreRenderer to filter out UsageHintGroup children when rendering proof explanations. Added a test to verify that usage hints are not included in the output for proof explanations.
Removes filtering of UsageHintGroup in DefaultProofExplanationTextPreRenderer and updates DefaultUsageHintGroupTextPreRenderer to skip rendering when explaining proof. Adds a test to verify usage hints are not rendered in proof explanations as direct and not-direct children.
Introduced DontShowIfExplainingTextPreRenderer to suppress rendering of DebugGroup and UsageHintGroup when under a proof explanation. Added DefaultDebugGroupTextPreRenderer and DefaultUsageHintGroupTextPreRenderer to use this new base class. Added and extended tests to verify that debug and usage hint groups are not shown within proof explanations.
Author
|
@robstoll i created the abstract class also and now a debugGroup is also not visible in the reporter when inside a ProofExplanation |
Owner
|
@WesleyJammer I currently don't have time to rebase the feature/proof-based-reporter branch on main but your changes look good. Going to merge them. Thanks for your first contribution to Atrium 🙂 👍 |
robstoll
merged commit 4547dd0
into
robstoll:feature/proof-based-reporter
2 of 12 checks passed
Author
|
@robstoll also thanks for helping me with the contribution! |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Introduced DontShowIfExplainingTextPreRenderer to suppress rendering of DebugGroup and UsageHintGroup when under a proof explanation. Added DefaultDebugGroupTextPreRenderer and DefaultUsageHintGroupTextPreRenderer to use this new base class. Added and extended tests to verify that debug and usage hint groups are not shown within proof explanations.
I confirm that I have read the Contributor Agreements v1.0, agree to be bound on them and confirm that my contribution is compliant.