doc/...: Fix `\textbar' properly, and use plain `|'.
authorMark Wooding <mdw@distorted.org.uk>
Sat, 24 Aug 2019 16:14:51 +0000 (17:14 +0100)
committerMark Wooding <mdw@distorted.org.uk>
Sat, 24 Aug 2019 20:53:17 +0000 (21:53 +0100)
commitb04739d01153eb539fd6b05095368e60b0d32bf6
tree82379f2b659a907ed57628ceed3351601ae2ad8d
parent3934b7ee2c441fc30d64e401facd0e798fe4978f
doc/...: Fix `\textbar' properly, and use plain `|'.

The `\grammar' command wasn't the right place to hack this, since
`\syntax' also needs fixing.  Instead, patch `\syn@shorts' to do the
right thing.

Once this is done, use `|' rather than `@|' in syntax displays (not the
Lisp ones!).  Also, use text rather than maths spacing consistently, by
replacing `$| \cdots |$' with `| $\cdots$ |' throughout.
doc/refintro.tex
doc/sod.sty
doc/syntax.tex