The built-in 'literal' role implements ``. It tokenizes the
literal string to attempt some particular wrapping behavior.
This puts parts of the string in different spans, each with
class='pre' and the previous docs.css had a padding for that
class. This led to excessive space within the literal string.
The custom role does no do this tokenization, but nested
inline parsing can result in multiple nodes, repeating the
problem. So, the padding for class='pre' is dropped. Ideally,
the sequence of nodes would simply be wrapped in an inline element
with class='pre' or some other proper solution that avoids having
multiple nodes.
To avoid wrapping in the middle of a literal, the 'pre' class
now has the style `white-space: pre;`.
The default role is now 'codeliteral' and the previous
uses of the built-in `` are converted to `. Some incorrectly
converted code blocks were fixed in the process.
Finally, the Global-Settings page is updated with the new location
for the global sbt directory. Due to the above changes, this could
be done without hardcoding the version.
Bruno Bieth
Mark Harrah