Fix compile warnings: Doc string single quote#863
Merged
Matafou merged 6 commits intoProofGeneral:masterfrom Jan 24, 2026
Merged
Fix compile warnings: Doc string single quote#863Matafou merged 6 commits intoProofGeneral:masterfrom
Matafou merged 6 commits intoProofGeneral:masterfrom
Conversation
See this quote from the Info page "(elisp) Documentation Tips": Some previous versions of this section recommended using the non-ASCII single quotation marks directly in doc strings, but this is now discouraged, since that leads to broken help string displays on terminals that don’t support displaying those characters.
On modern Emacsen this is a compile time warning. Before this change there where 111 of these warnings. Now there are 7.
Now that symbols are quoted more carefully we can remove some of the complicated heuristic rules that had some false positives (like treating the word "top-level" as a symbol) and replace them with some pretty simple rules. This changes the markup of many symbols from @samp{@code{SYM}} to @code{SYM}.
Update doc/PG-adapting.texi and doc/ProofGeneral.texi using the command "make -C doc magic"
Contributor
|
Thanks! |
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
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.
Hello again!
When compiling proof general there are over 400 warnings! Some of these warnings might be important but it is hard to tell with this much noise. I would like to help reduce this noise.
Newer emacs emit warnings when that are unescaped single quotes in docstrings. I've spent a good chunk of time resolving this issue.
For symbols that link to a variable or function they should be written as: `symbol'
For symbols that should not link to anything as they are just a symbol they should be written as: \+`symbol'.
By going through and making sure symbols are quoted using this style, I was also able to simplify the documentation generator slightly which removes some false positives and removes a lot of "@samp{@code{symbol}}" and replaces it with "@code{symbol}" which seems better.