*Yamma 0.0.17 Released:*
*Management of Discouraged Theorems*: New features have been added to help
users handle discouraged theorems more effectively.
*Enhanced Step Suggestions*: Step suggestions are now fully filtered on the
server side, ensuring that VSCode does not apply additional filtering. This
resolves the issue where useful label suggestions were being inadvertently
excluded by VSCode, making them visible to users again.
*### Version 0.0.17 (2025-01-25)*
*#### Added*
- A new diagnostic warning is added when a .mmp proof step is justified
using a label that refers to a statement with a 'new usage is discouraged'
tag.
- Introduced the `$allowdiscouraged` directive in .mmp proofs.
- Proofs containing this directive will bypass warnings when using
labels tagged with 'new usage is discouraged.'
- Proofs with the `$allowdiscouraged` directive will be generated if
they are complete.
- The new diagnostic warning contains a 'Quick Fix' that automatically
adds the $allowdiscouraged directive
*#### Changed*
Proofs that use labels tagged as 'new usage is discouraged' are no longer
generated, even if complete, unless the `$allowdiscouraged` flag is present.
*#### Improved*
CompletionItems for step suggestions are now completely filtered on the
server and additional client side filtering is disabled (previously, useful
label suggestions were filtered out by VSCode, and not shown to the user)
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion visit
https://groups.google.com/d/msgid/metamath/78f73e0b-5ca1-4ad2-9a81-32bd90d0a11bn%40googlegroups.com.
