In fact it is sufficient to have multiple stylesheets and load the one you want
to switch to. The problem is that we probably want to remember the set color
scheme for longer than just the current page, so we'd need something like
cookies.
We could also do this without JS by generating multiple versions of the docs
referencing different stylesheet.
Of course this would kind of blow up the size of the documentation for changing
a single line.
Sadly the browser functionality for multiple stylesheets usually consists of an
obscure list hidden in some menu.
In my opinion the best thing would be if the browser did some notification like
"This page offers multiple styles" along with some selector. But as things are
we can only do this either dynamically on the server (which we probably do not
want), dynamically on the client by JS (which we probably don't want) or
statically by with multiple versions (which would be rather unelegant).
Cheers,
Valentin
04.01.2022 17:23:59 Aaron Hill <lilyp...@hillvisions.com>:
> On 2022-01-04 7:29 am, Erika Pirnes wrote:
>> Would it be terribly difficult to have a color setting on the
>> documentation page, so that people can choose between black and color?
>
> It is fairly straightforward with CSS and a little JavaScript:
>
>
> <!DOCTYPE html>
> <html lang="en">
> <head>
> <meta charset="UTF-8">
> <meta http-equiv="X-UA-Compatible" content="IE=edge">
> <meta name="viewport" content="width=device-width, initial-scale=1.0">
> <title>Dynamic styles</title>
> <style>
> body { font-size: 36pt; }
> .button {
> background: #999; border-radius: 9pt;
> cursor: pointer; display: inline-block;
> padding: 9pt; user-select: none;
> }
> .colors > code > .type { color: purple; }
> .colors > code > .identifier { color: blue; }
> .colors > code > .keyword { color: brown; }
> .colors > code > .number { color: darkgoldenrod; }
> .colors > code > .string { color: green; }
> .colors > code > .punctuation { color: gray; }
> </style>
> </head>
> <body>
> <script>
> function toggleColors() {
> if (document.body.classList.contains('colors')) {
> document.body.classList.remove('colors');
> } else {
> document.body.classList.add('colors');
> }
> }
> </script>
> <div class="button" onclick="toggleColors()">Toggle Colors</div><br/>
>
> <code>
> <span class="type">int</span>
> <span class="identifier">main</span><span class="punctuation">()
> {</span><br/>
> <span class="identifier">printf</span><span
> class="punctuation">(</span><span class="string">"Hello,
> World!\n"</span><span class="punctuation">);</span><br/>
> <span class="keyword">return</span>
> <span class="number">0</span><span class="punctuation">;</span><br/>
> <span class="punctuation">}</span>
> </code>
> </body>
> </html>
>
>
> -- Aaron Hill
