body.hook
{ 
    font-family: "Times", serif;
    background: white;
    margin-left: 3.0em;
    margin-right: 0.5em;
}

h1
{
    border-top: thick solid gray;
    padding: 0.5em 0em 0em 0em;    
    color: darkblue;
    font-style: normal;
    font-weight: bold;
    font-size: 2em;
}

h2
{
    border-top: thin solid gray;
    padding: 0.5em 0em 0em 0em;
    color: darkblue;
    font-style: normal; 
    font-weight: bold;
    font-size: 1.5em;
}


h3
{
    padding: 0.5em 0em 0em 0em;
    color: darkblue;
    font-style: normal; 
    font-weight: bold;
    font-size: 1.2em;
}


h4
{
    padding: 0.5em 0em 0em 0em;
    color: darkblue;
    font-style: normal; 
    font-weight: bold;
    font-size: 1.0em;
}

p
{
    font-size: 1.0em;
    font-family: "Times", serif;
    font-weight: 100;
}

pre.shell
{
    font-size: 0.8em;
    font-family: "Courier New", Courier, monospace;
    font-weight: bold;
    background-color: dimgray;
    color: white;
    padding: 0.7em 0.7em 0.7em 0.7em;
    margin: 1em 1em 1em 2em;    
}

span.opening-quote
{
    display: block;
    margin-left: 50%;
    text-align: right;
}

span.opening-quote.quote-source
{
    display: block;
    text-align: right;
    font-style: italic;
    color: darkblue;
}

span.filename
{
    display: block;
    text-align: right;
    font-size: 0.8em;
    font-style: italic;
    font-family: "Courier New", Courier, monospace;
    margin: 1em 1em 1em 2em;
}

pre.code
{ 
    font-size: 0.8em;
    font-family: "Courier New", Courier, monospace;
    font-weight: normal;
    background-color: #E6E6FA; /* Lavendar */ 
    padding: 0.7em 0.7em 0.7em 0.7em;
    margin: 1em 1em 1em 2em;
}

pre.fragment
{
    font-size: 0.8em;
    font-family: "Courier New", Courier, monospace;
    font-weight: normal;
    background-color: #E6E6FA; /* Lavendar */ 
    padding: 1em 1em 1em 1em;
    /* border-right: 1 solid gray; */
    padding: 0.7em 0.7em 0.7em 0.7em;
    margin: 1em 1em 1em 2em;
    /*border-left: 3 solid gray;
    border-right: 3 solid gray;
    border-top: 3 solid gray;
    border-bottom: 3 solid gray;*/

}

pre.grammar
{
    font-size: 0.8em;
    font-family: "Courier New", Courier, monospace;
    font-weight: 100;
    background-color: white; 
    padding: 1em 1em 1em 1em;
    border: 1 solid gray;
    padding: 0.7em 0.7em 0.7em 0.7em;
    margin: 1em 1em 1em 2em;
}

sup.power
{
    font-size: 0.5em;
}

span.guideline
{
    display: block;    
    border-right: 3 solid gray;
    border-bottom: 3 solid gray;    
    padding: 1em 1em 1em 1em;
    margin: 1em 0em;
    background-color: #C0C0FF;    
}

span.guideline.title
{
    font-size: 1.2em;
    color: darkblue;
}

span.term 
{
    font-style: italic;
    color: blue;
}

span.motto
{
    font-style: italic;
    color: blue;
}

span.emphasis
{
    font-style: italic;
}

span.footnote
{
    color: red;
}

span.book-reference
{
    color: green;
}

span.quote 
{
    quotes: '"';
    display: inline;
}

span.directive
{
    color: gray;
}

span.identifier
{
    color: black;
}

span.keyword
{
    color: darkblue;
}

span.literal
{
    color: green;   
}

span.punctuator
{
    color: black;
}

span.comment
{
    color: green;
    font-family: "Arial", sans-serif;
    font-style: italic;
    font-weight: normal;
}

span.other
{
    color: red; /* shouldn't happen */
}