Skip to content

Conversation

@MorganJamesSmith
Copy link
Contributor

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.

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"
@Matafou Matafou merged commit 75c13f9 into ProofGeneral:master Jan 24, 2026
140 checks passed
@Matafou
Copy link
Contributor

Matafou commented Jan 24, 2026

Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants