1 | @CHARSET "ISO-8859-1";
|
---|
2 | /*
|
---|
3 | * This is the CSS file used in the internal help browser.
|
---|
4 | * Refer to https://docs.oracle.com/javase/8/docs/api/javax/swing/text/html/CSS.html
|
---|
5 | * and https://www.w3.org/TR/CSS1/ to see what CSS properties are supported by Java.
|
---|
6 | * - Not rendered are width, height, float, clear, display, font-variant and others.
|
---|
7 | * - Inline elements can't have borders, margins and paddings.
|
---|
8 | */
|
---|
9 | body {margin-left: 0.2cm; font-family: Arial, sans-serif; font-size:14pt; font-weight:normal}
|
---|
10 | p {margin-top: 5px; margin-bottom: 5px;}
|
---|
11 | h1 {font-family: Arial, sans-serif; font-size:24pt; font-weight:bold}
|
---|
12 | h2 {margin-top: 14pt; font-family: Arial, sans-serif; font-size:20pt; font-weight:bold}
|
---|
13 | h3 {margin-top: 14pt; font-family: Arial, sans-serif; font-size:16pt; font-weight:bold}
|
---|
14 | h4 {margin-top: 14pt; font-family: Arial, sans-serif; font-size:14pt; font-weight:bold}
|
---|
15 | a {font-family: Arial, sans-serif; font-size:14pt; font-weight:normal; text-decoration: underline; color: blue}
|
---|
16 | ul {margin-left: 1cm; list-style-type: disc}
|
---|
17 | ul ul {margin-left: 1cm; list-style-type: circle}
|
---|
18 | ol {margin-left: 1cm;}
|
---|
19 | strong {font-weight: bold}
|
---|
20 | b {font-weight: bold}
|
---|
21 | em {font-style: italic}
|
---|
22 | i {font-style: italic}
|
---|
23 | code, pre, samp, tt {font-family: Courier New}
|
---|
24 | code, tt {
|
---|
25 | background-color: rgb(240, 240, 240);
|
---|
26 | font-size: 110%;
|
---|
27 | color: rgb(102, 0, 0);
|
---|
28 | }
|
---|
29 | .warning-header {
|
---|
30 | font-family: Arial, sans-serif;
|
---|
31 | font-size:24pt;
|
---|
32 | font-weight:bold
|
---|
33 | }
|
---|
34 | .warning-body {
|
---|
35 | background-color:rgb(253,255,221);
|
---|
36 | padding: 10pt;
|
---|
37 | border-color:rgb(128,128,128);
|
---|
38 | border-style: solid;
|
---|
39 | border-width: 1px;
|
---|
40 | }
|
---|
41 |
|
---|
42 | .error-header {
|
---|
43 | font-family: Arial, sans-serif;
|
---|
44 | font-size:24pt;
|
---|
45 | font-weight:bold
|
---|
46 | }
|
---|
47 | .error-body {
|
---|
48 | background-color:rgb(254,195,190);
|
---|
49 | padding: 10pt;
|
---|
50 | border-color:rgb(128,128,128);
|
---|
51 | border-style: solid;
|
---|
52 | border-width: 1px;
|
---|
53 | }
|
---|