strip attempts to make HTML fonts nice

svn: r8297

original commit: 47621b088b7101a5979423c6a68e4ffbc5a54681
This commit is contained in:
Matthew Flatt 2008-01-11 11:44:01 +00:00
parent f69d5a49c3
commit b4f706247f
2 changed files with 29 additions and 29 deletions

View File

@ -423,7 +423,7 @@
(case style (case style
[(italic) `((i ,@(super render-element e part ri)))] [(italic) `((i ,@(super render-element e part ri)))]
[(bold) `((b ,@(super render-element e part ri)))] [(bold) `((b ,@(super render-element e part ri)))]
[(tt) `((tt ,@(super render-element e part ri)))] [(tt) `((span ([class "stt"]) ,@(super render-element e part ri)))]
[(no-break) `((span ([class "nobreak"]) ,@(super render-element e part ri)))] [(no-break) `((span ([class "nobreak"]) ,@(super render-element e part ri)))]
[(sf) `((b (font ([size "-1"][face "Helvetica"]) ,@(super render-element e part ri))))] [(sf) `((b (font ([size "-1"][face "Helvetica"]) ,@(super render-element e part ri))))]
[(subscript) `((sub ,@(super render-element e part ri)))] [(subscript) `((sub ,@(super render-element e part ri)))]

View File

@ -10,14 +10,14 @@
} }
.maincolumn { .maincolumn {
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
width: 43em; width: 43em;
margin-right: -40em; margin-right: -40em;
margin-left: 15em; margin-left: 15em;
} }
.main { .main {
font-family: Times, serif; font-size: 16px; font-family: serif;
text-align: left; text-align: left;
} }
@ -32,11 +32,11 @@
} }
.version { .version {
font-family: sans-serif; font-family: sans-serif;
font-size: 13px;
} }
.refpara { .refpara {
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
position: relative; position: relative;
float: right; float: right;
left: 1em; left: 1em;
@ -56,11 +56,11 @@
} }
.refcontent { .refcontent {
font-family: Times, serif; font-size: 13px; font-family: serif;
} }
.tocset { .tocset {
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
position: relative; position: relative;
float: left; float: left;
width: 12.5em; width: 12.5em;
@ -68,13 +68,13 @@
} }
.tocview { .tocview {
font-family: Times, serif; font-size: 16px; font-family: serif;
text-align: left; text-align: left;
background-color: #F5F5DC; background-color: #F5F5DC;
} }
.tocsub { .tocsub {
font-family: Times, serif; font-size: 16px; font-family: serif;
margin-top: 1em; margin-top: 1em;
text-align: left; text-align: left;
background-color: #DCF5F5; background-color: #DCF5F5;
@ -176,6 +176,10 @@
white-space: nowrap; white-space: nowrap;
} }
.stt {
font-family: monospace;
}
.title { .title {
font-size: 200%; font-size: 200%;
font-weight: normal; font-weight: normal;
@ -259,12 +263,8 @@
list-style-type: upper-alpha; list-style-type: upper-alpha;
} }
tt {
font-family: Consolas, Courier, monospace; font-size: 13px;
}
i { i {
font-family: Times, serif; font-family: serif;
} }
.boxed { .boxed {
@ -296,7 +296,7 @@
} }
.verbatim em { .verbatim em {
font-family: Times, serif; font-family: serif;
} }
.ghost { .ghost {
@ -305,7 +305,7 @@
.scheme em { .scheme em {
color: black; color: black;
font-family: Times, serif; font-family: serif;
} }
.highlighted { .highlighted {
@ -322,7 +322,7 @@
} }
.hspace { .hspace {
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.small { .small {
@ -340,7 +340,7 @@
.schemeinput { .schemeinput {
color: brown; color: brown;
background-color: #eeeeee; background-color: #eeeeee;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemeinputbg { .schemeinputbg {
@ -348,22 +348,22 @@
} }
.schemereader { .schemereader {
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemeparen { .schemeparen {
color: #843c24; color: #843c24;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schememeta { .schememeta {
color: #262680; color: #262680;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schememod { .schememod {
color: black; color: black;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemeopt { .schemeopt {
@ -373,7 +373,7 @@
.schemekeyword { .schemekeyword {
color: black; color: black;
font-weight: bold; font-weight: bold;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemeerror { .schemeerror {
@ -384,12 +384,12 @@
.schemevariable { .schemevariable {
color: #262680; color: #262680;
font-style: italic; font-style: italic;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemesymbol { .schemesymbol {
color: #262680; color: #262680;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemevaluelink { .schemevaluelink {
@ -429,22 +429,22 @@
.schemeresult { .schemeresult {
color: #0000af; color: #0000af;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemestdout { .schemestdout {
color: #960096; color: #960096;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemecomment { .schemecomment {
color: #c2741f; color: #c2741f;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.schemevalue { .schemevalue {
color: #228b22; color: #228b22;
font-family: Consolas, Courier, monospace; font-size: 13px; font-family: monospace;
} }
.bibliography td { .bibliography td {