Skip to content

Commit 62e63a6

Browse files
EelisEelis
committed
Quote font family names containing whitespace in CSS.
Fixes #106.
1 parent 390d4c3 commit 62e63a6

File tree

3 files changed

+39
-39
lines changed

3 files changed

+39
-39
lines changed

‎14882.css

Lines changed: 35 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,5 @@
11
body {
2-
font-family: Noto Serif;
2+
font-family: 'Noto Serif';
33
hyphens: auto;
44
line-height: 1.5;
55
margin-left: 20mm;
@@ -208,7 +208,7 @@ div.itemdescr {
208208
}
209209

210210
.bnf {
211-
font-family: Noto Sans;
211+
font-family: 'Noto Sans';
212212
font-size: 10pt;
213213
font-style: italic;
214214
margin-left: 25pt;
@@ -220,10 +220,10 @@ div.itemdescr {
220220
line-height: 1.5;
221221
}
222222

223-
div.bnf span.texttt { font-family: Noto Sans Mono; font-style: normal; }
223+
div.bnf span.texttt { font-family: 'Noto Sans Mono'; font-style: normal; }
224224

225225
.rebnf {
226-
font-family: Noto Serif;
226+
font-family: 'Noto Serif';
227227
font-style: italic;
228228
margin-top: 0.5em;
229229
margin-bottom: 0.5em;
@@ -234,7 +234,7 @@ div.bnf span.texttt { font-family: Noto Sans Mono; font-style: normal; }
234234
}
235235

236236
.simplebnf {
237-
font-family: Noto Serif;
237+
font-family: 'Noto Serif';
238238
font-style: italic;
239239
font-size: 10pt;
240240
margin-top: 0.5em;
@@ -245,14 +245,14 @@ div.bnf span.texttt { font-family: Noto Sans Mono; font-style: normal; }
245245

246246
span.textnormal {
247247
font-style: normal;
248-
font-family: Noto Serif;
248+
font-family: 'Noto Serif';
249249
font-size: 10pt;
250250
white-space: normal;
251251
}
252252

253253
.bnf span.textnormal {
254254
font-style: normal;
255-
font-family: Noto Serif;
255+
font-family: 'Noto Serif';
256256
font-size: 10pt;
257257
white-space: normal;
258258
}
@@ -269,42 +269,42 @@ span.rlap {
269269
}
270270

271271
span.terminal {
272-
font-family: Noto Sans Mono;
272+
font-family: 'Noto Sans Mono';
273273
font-style: normal;
274274
font-size: 9pt;
275275
white-space: pre-wrap;
276276
}
277277

278278
span.noncxxterminal {
279-
font-family: Noto Sans Mono;
279+
font-family: 'Noto Sans Mono';
280280
font-style: normal;
281281
font-size: 9pt;
282282
}
283283

284284
span.term { font-style: italic; }
285-
span.tcode { font-family: Noto Sans Mono; font-style: normal; }
285+
span.tcode { font-family: 'Noto Sans Mono'; font-style: normal; }
286286
span.textbf { font-weight: bold; }
287-
span.textsf { font-family: Noto Sans; font-size: 10pt; }
288-
div.footnote span.textsf { font-family: Noto Sans; font-size: 8pt; }
289-
.bnf span.textsf { font-family: Noto Sans; font-size: 10pt; }
290-
.simplebnf span.textsf { font-family: Noto Sans; font-size: 10pt; }
291-
.example span.textsf { font-family: Noto Sans; font-size: 10pt; }
287+
span.textsf { font-family: 'Noto Sans'; font-size: 10pt; }
288+
div.footnote span.textsf { font-family: 'Noto Sans'; font-size: 8pt; }
289+
.bnf span.textsf { font-family: 'Noto Sans'; font-size: 10pt; }
290+
.simplebnf span.textsf { font-family: 'Noto Sans'; font-size: 10pt; }
291+
.example span.textsf { font-family: 'Noto Sans'; font-size: 10pt; }
292292
span.textsc { font-variant: small-caps; }
293-
span.nontermdef { font-style: italic; font-family: Noto Sans; font-size: 10pt; }
294-
.rebnf a.nontermdef { font-style: italic; font-family: Noto Serif; }
293+
span.nontermdef { font-style: italic; font-family: 'Noto Sans'; font-size: 10pt; }
294+
.rebnf a.nontermdef { font-style: italic; font-family: 'Noto Serif'; }
295295
span.emph { font-style: italic; }
296296
span.techterm { font-style: italic; }
297297
span.mathit { font-style: italic; }
298-
span.mathsf { font-family: Noto Sans; }
299-
span.mathrm { font-family: Noto Serif; font-style: normal; }
300-
span.textrm { font-family: Noto Serif; font-size: 10pt; }
298+
span.mathsf { font-family: 'Noto Sans'; }
299+
span.mathrm { font-family: 'Noto Serif'; font-style: normal; }
300+
span.textrm { font-family: 'Noto Serif'; font-size: 10pt; }
301301
span.textsl { font-style: italic; }
302-
span.mathtt { font-family: Noto Sans Mono; font-style: normal; }
303-
span.mbox { font-family: Noto Serif; font-style: normal; }
302+
span.mathtt { font-family: 'Noto Sans Mono'; font-style: normal; }
303+
span.mbox { font-family: 'Noto Serif'; font-style: normal; }
304304
span.ungap { display: inline-block; width: 2pt; }
305-
span.texttt { font-family: Noto Sans Mono; }
306-
div.footnote span.texttt { font-family: Noto Sans Mono; }
307-
span.tcode_in_codeblock { font-family: Noto Sans Mono; font-style: normal; font-size: 9pt; }
305+
span.texttt { font-family: 'Noto Sans Mono'; }
306+
div.footnote span.texttt { font-family: 'Noto Sans Mono'; }
307+
span.tcode_in_codeblock { font-family: 'Noto Sans Mono'; font-style: normal; font-size: 9pt; }
308308

309309
span.phantom { color: white; }
310310
/* Unfortunately, this way the text is still selectable. Another
@@ -313,7 +313,7 @@ span.phantom { color: white; }
313313

314314
span.math {
315315
font-style: normal;
316-
font-family: Noto Serif;
316+
font-family: 'Noto Serif';
317317
font-size: 10pt;
318318
}
319319

@@ -342,7 +342,7 @@ span.definition {
342342
}
343343

344344
.codeblock {
345-
font-family: Noto Sans Mono;
345+
font-family: 'Noto Sans Mono';
346346
margin-left: 1.2em;
347347
line-height: 1.5;
348348
font-size: 9pt;
@@ -359,12 +359,12 @@ table .codeblock { margin-right: 0; }
359359
.outputblock {
360360
margin-left: 1.2em;
361361
line-height: 1.5;
362-
font-family: Noto Sans Mono;
362+
font-family: 'Noto Sans Mono';
363363
font-size: 9pt;
364364
}
365365

366366
code {
367-
font-family: Noto Sans Mono;
367+
font-family: 'Noto Sans Mono';
368368
font-style: normal;
369369
}
370370

@@ -374,24 +374,24 @@ div.itemdecl {
374374

375375
code.itemdeclcode {
376376
white-space: pre;
377-
font-family: Noto Sans Mono;
377+
font-family: 'Noto Sans Mono';
378378
font-size: 9pt;
379379
display: block;
380380
overflow: auto;
381381
margin-right: -15mm;
382382
}
383383

384-
.comment { color: green; font-style: italic; font-family: Noto Serif; font-size: 10pt; }
385-
.footnote .comment { color: green; font-style: italic; font-family: Noto Serif; font-size: 8pt; }
386-
.example .comment { color: green; font-style: italic; font-family: Noto Serif; font-size: 9pt; }
387-
.note .comment { color: green; font-style: italic; font-family: Noto Serif; font-size: 9pt; }
384+
.comment { color: green; font-style: italic; font-family: 'Noto Serif'; font-size: 10pt; }
385+
.footnote .comment { color: green; font-style: italic; font-family: 'Noto Serif'; font-size: 8pt; }
386+
.example .comment { color: green; font-style: italic; font-family: 'Noto Serif'; font-size: 9pt; }
387+
.note .comment { color: green; font-style: italic; font-family: 'Noto Serif'; font-size: 9pt; }
388388

389389
span.keyword { color: #00607c; font-style: normal; }
390390
span.parenthesis { color: #af1915; }
391391
span.curlybracket { color: #af1915; }
392392
span.squarebracket { color: #af1915; }
393393
span.literal { color: #9F6807; }
394-
span.literalterminal { color: #9F6807; font-family: Noto Sans Mono; font-style: normal; }
394+
span.literalterminal { color: #9F6807; font-family: 'Noto Sans Mono'; font-style: normal; }
395395
span.operator { color: #570057; }
396396
span.anglebracket { color: #570057; }
397397
span.preprocessordirective { color: #6F4E37; }

‎SectionPages.hs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -230,10 +230,10 @@ writeCssFile = do
230230
replaceFonts =
231231
Text.replace
232232
".MJXc-TeX-sans-R {font-family: MJXc-TeX-sans-R,MJXc-TeX-sans-Rw}"
233-
".MJXc-TeX-sans-R {font-family: Noto Sans; font-size: 10pt; }" .
233+
".MJXc-TeX-sans-R {font-family: 'Noto Sans'; font-size: 10pt; }" .
234234
Text.replace
235235
".MJXc-TeX-type-R {font-family: MJXc-TeX-type-R,MJXc-TeX-type-Rw}"
236-
".MJXc-TeX-type-R {font-family: Noto Sans Mono; font-size: 10pt; }" .
236+
".MJXc-TeX-type-R {font-family: 'Noto Sans Mono'; font-size: 10pt; }" .
237237
Text.replace
238238
".MJXc-TeX-main-R {font-family: MJXc-TeX-main-R,MJXc-TeX-main-Rw}"
239239
".MJXc-TeX-main-R {}" .

‎expanded.css

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,8 +15,8 @@ div.note {
1515
div.note .texttt { font-size: 9pt; }
1616
div.example .texttt { font-size: 9pt; }
1717

18-
div.note .textsf { font-family: Noto Sans; font-size: 9pt; }
19-
div.example .textsf { font-family: Noto Sans; font-size: 9pt; }
18+
div.note .textsf { font-family: 'Noto Sans'; font-size: 9pt; }
19+
div.example .textsf { font-family: 'Noto Sans'; font-size: 9pt; }
2020

2121
div.note .math { font-size: 9pt; }
2222
div.example .math { font-size: 9pt; }

0 commit comments

Comments
 (0)