body
{
    background-color: #909090; /* Light Grey background color for the document */
    margin-top: 4em;           /* Make room for the div.top elements in the top margin*/
    padding-left: 11em;
}

h1
{
    color: black;
    background-color: #b00000;
    border-bottom-width: 5px;
    border-bottom-color: black;
    border-bottom-style: solid;
    padding-left: 0.25em;
}

.code
{
/*    margin-left: 1em;*/
    width: page;
    font-family: monospace;
    background-color: black;
    color: #30ff30;
    padding: 0.5em 0.5em 0.5em 0.5em ;
    overflow: auto;
}

.replace
{
    color: red;
}

#top
{
    position: absolute;
    top: 0px;
    left: 0px;
    width: 100%;
    height: 3em;
    background-color: #606060;
}

#left
{
    position: absolute;
    top: 4em;
    left: 0;
    height: auto;
    width: 10em;
    background-color: #606060;
    margin-left: 0.5em;
    padding-bottom: 1em;
    padding-top: 1em;
}


.leftmenuentry
{
    margin-right: 0.5em;
    margin-left: 0.5em;
    margin-top: 0.5em;
    margin-bottom: 0.5em;
    padding-top: 0.1em;
    padding-bottom: 0.1em;
/*    background-color: #909090; */
}


/************/
/* Top Menu */
/************/

/* The menu placed at the right side of the top */
span#topmenu
{
    position: absolute;
    float: right;
    text-align: right;
    top: 1.8em;
    right: 0;
/*    background-color: pink;*/
}

/* The buttons/entries in the menu */
span.topmenuentry
{
    background-color: #909090;
    /* Put some space between the menu-entries */
    margin-left: 0.25em;
    margin-right: 0.25em;
    /* Make the grey (#909090) boxes around the link a little wider than the link text */
    padding-left: 0.5em;  
    padding-right: 0.5em;
}

/* The "logo like" name on the top left */
span#myname
{
    position: absolute;
    top: 0;
    font-size: 3em;
    margin-left: 0.1em; 
    color: #b00000;
}


/*********/
/* Links */
/*********/

/* Avoid lines under the links */
a
{
    text-decoration: none;
    color: black;
}

a:focus, a:active
{
    outline-width: 0px;
    color: #ffffff;
}

a:visited
{
    color: #204040;
}

/* Make the link texts red when hovering over the link */
a:hover
{
    color: #ff0000;
}