On Wed, Feb 27, 2019 at 12:03 PM David Storrs <david.sto...@gmail.com> wrote:
>
> I have a .scrbl file with the following:
>
> @verbatim{
> ...stuff...
> | #:rule (rule-name #:transform field-id
> (field-id ...+) (code ...+))
> }
>
> My expectation is that this will render, well, verbatim. Instead, it
> adds a line break so that I get:
>
> | #:rule (rule-name #:transform field-id (field-id
> ...+) (code ...+))
>
> Am I not understanding something?
Found the problem: The manual.scrbl file uses pixel-based max widths.
This seems odd, since the CSS is generally defined using rems, which
is a much better solution.
>
>
> Separately, a comment on the HTML that is generated from Scribble:
>
> It uses table-based layout and then adds CSS on top of that. This seems odd.
>
> The standard scribble.css file includes the following comment:
>
> ===quote
> /* CSS seems backward: List all the classes for which we want a
> particular font, so that the font can be changed in one place. (It
> would be nicer to reference a font definition from all the places
> that we want it.)
>
> As you read the rest of the file, remember to double-check here to
> see if any font is set. */
> ===/quote
>
> It's perfectly legit to do it the other way around, and in fact that's
> the more standard way. Instead of putting this at the top of the
> file:
>
> /* Monospace: */
> .maincolumn, .refpara, .refelem, .tocset, .stt, .hspace, .refparaleft,
> .refelemleft {
> font-family: monospace;
> }
>
> It's fine to do this:
>
> .maincolumn { font-family: monospace }
> .refpara { font-family: monospace }
>
>
> Also, it would be really spiffy if the generated HTML was
> pretty-printed. Having it minified seems unnecessary and
> disadvantageous.
>
> Are these things that people are open to changing and, if so, is there
> a way I can help?
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to racket-users+unsubscr...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.
