fix some rendering problems when printing

This commit is contained in:
2022-06-20 16:39:54 +02:00
parent fdfa4d4695
commit 2915830b02

View File

@ -12,7 +12,15 @@ body {
background-color: #ffffff; background-color: #ffffff;
} }
a[name] { position:relative; top:-11ex;} a[name] {
position: relative;
top: -11ex;
}
pre, tt, kbd, code {
font-size: 95%;
font-family: Mono, "Lucida Console", Courier, monospace;
}
pre { pre {
background-color: #f4f4f4; background-color: #f4f4f4;
@ -21,12 +29,18 @@ pre {
white-space: pre; white-space: pre;
margin: 2ex; margin: 2ex;
page-break-inside: avoid; page-break-inside: avoid;
font-size: 85%;
white-space: pre-wrap;
} }
kbd { kbd {
font-weight: bold; font-weight: bold;
} }
code {
color: #008000;
}
dt { dt {
margin-top: 0.5ex; margin-top: 0.5ex;
} }
@ -36,7 +50,7 @@ h1 {
margin-top: 0; margin-top: 0;
font-style: italic; font-style: italic;
font-weight: bold; font-weight: bold;
font-family:"Times New Roman", serif; font-family: "Times New Roman", Times, serif;
text-align: center; text-align: center;
position: fixed; position: fixed;
top: 0; top: 0;
@ -50,12 +64,12 @@ h1 {
background-image: url(PSI.png); background-image: url(PSI.png);
background-repeat: no-repeat; background-repeat: no-repeat;
background-position: 10px 5px; background-position: 10px 5px;
text-shadow:.1em .1em .1em darkgray; text-shadow: .1em .1em .1em lightgray;
box-shadow: 0 .3em .1em -.2em darkgray; box-shadow: 0 .3em .1em -.2em darkgray;
} }
h2 { h2 {
font-size:150%; font-size: 140%;
margin-bottom: 0.5ex; margin-bottom: 0.5ex;
} }
@ -100,11 +114,6 @@ small {
font-size: 75%; font-size: 75%;
} }
code {
font-size: 125%;
color: #008000;
}
.indent { .indent {
text-indent: -4ex; text-indent: -4ex;
margin-left: 4ex; margin-left: 4ex;
@ -117,9 +126,10 @@ code {
margin-right: 1ex; margin-right: 1ex;
margin-top: 0.5ex; margin-top: 0.5ex;
padding: 0 1ex; padding: 0 1ex;
border: 1px solid black; border: thin solid black;
text-align: left; text-align: left;
background-color: #f0f0f0; background-color: #f0f0f0;
page-break-inside: avoid;
} }
#navleft { #navleft {
@ -151,8 +161,9 @@ a[target=ex]:hover:after {
@media print { @media print {
a:link { text-decoration: none; } a:link { text-decoration: none; }
a[target=ex]:after {content:" [" attr(href) "]";} a[target=ex]:after { content:" [" attr(href) "]"; font-size: 75%; }
body { margin: 0 4em; } body { margin: 0 4em; }
h1 { position: relative; background-position: 0 0; } h1 { position: relative; background-position: 0 0; }
#navleft { display: none; } #navleft { display: none; }
footer { display: none; }
} }