File: manual.css

package info (click to toggle)
maxima 5.21.1-2squeeze
  • links: PTS
  • area: main
  • in suites: squeeze
  • size: 94,928 kB
  • ctags: 43,849
  • sloc: lisp: 298,974; fortran: 14,666; perl: 14,325; tcl: 10,494; sh: 4,052; makefile: 2,975; ansic: 471; awk: 24; sed: 7
file content (100 lines) | stat: -rw-r--r-- 1,621 bytes parent folder | download | duplicates (11)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
body
{
    color: black;
    background: white; 
    margin-left: 8%;
    margin-right: 13%;
}

h1
{
    margin-left: +8%;
    font-size: 150%;
    font-family: sans-serif
}

h2
{
    font-size: 125%;
    font-family: sans-serif
}

h3
{
    font-size: 100%;
    font-family: sans-serif
}

h2,h3,h4,h5,h6 { margin-left: +4%; }

div.textbox
{
    border: solid;
    border-width: thin;
    /* width: 100%; */
    padding-top: 1em;
    padding-bottom: 1em;
    padding-left: 2em;
    padding-right: 2em
}

div.titlebox
{
    border: none;
    padding-top: 1em;
    padding-bottom: 1em;
    padding-left: 2em;
    padding-right: 2em;
    background: rgb(200,255,255);
    font-family: sans-serif
}

div.synopsisbox
{
    border: none;
    padding-top: 1em;
    padding-bottom: 1em;
    padding-left: 2em;
    padding-right: 2em;
     background: rgb(255,220,255);
    /*background: rgb(200,255,255); */
    /* font-family: fixed */
}

pre.example
{
    border: 1px solid gray;
    padding-top: 1em;
    padding-bottom: 1em;
    padding-left: 1em;
    padding-right: 1em;
    /* background: rgb(247,242,180); */ /* kind of sandy */
    /* background: rgb(200,255,255); */ /* sky blue */
    background-color: #F1F5F9; /* light blue-gray */
    /* font-family: "Lucida Console", monospace */
}

div.spacerbox
{
    border: none;
    padding-top: 2em;
    padding-bottom: 2em
}

div.image
{
    margin: 0;
    padding: 1em;
    text-align: center;
}

div.categorybox
{
    border: 1px solid gray;
    padding-top: 0px;
    padding-bottom: 0px;
    padding-left: 1em;
    padding-right: 1em;
    background: rgb(247,242,220);
}