123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103 |
- /* define a class "noprint" for sections which don't get printed */
- .noprint { display: none; }
- /* our syntax menu for switching */
- div.syntaxmenu {
- border: 1px dotted black;
- padding:0.5em;
- margin: 1em;
- }
- .container {
- margin-right: auto;
- margin-left: auto;
- padding-left: 15px;
- padding-right: 15px;
- }
- @media print {
- div.syntaxmenu { display:none; }
- }
- /* use tab-like headers for syntax examples */
- div.exampleheader {
- font-size: 90%;
- float: left;
- background: #F9F9F9;
- color: #2F6FAB;
- border: 1px dashed #2F6FAB;
- border-bottom: 0px;
- padding-top: 2px;
- }
- div.exampleheader span.exampleheader {
- background: #F9F9F9;
- padding-top: 0px;
- padding-right: 10px;
- padding-left: 10px;
- padding-bottom: 3px;
- padding-top: 0px;
- }
- /* Also copy MediaWiki style here, so it will not look different when exported */
- div.fssyntax pre, div.rdfxml pre, div.owlxml pre, div.turtle pre, div.manchester pre {
- background-color: #F9F9F9;
- border: 1px dashed #2F6FAB;
- color: black;
- line-height: 1.1em;
- padding: 1em;
- clear: both;
- margin-left: 0em;
- }
- /* Expansion to add the status*/
- .status {
- position: fixed;
- left: 0em;
- top: 0em;
- text-align: right;
- vertical-align: middle;
- /* Square version of the inside span. Slightly larger */
- width: 26em;
- height: 26em;
- z-index: -1;
- opacity: 0.8;
-
- /** From http://stackoverflow.com/questions/1080792/how-to-draw-vertical-text-with-css-cross-browser */
- -webkit-transform: rotate(-90deg);
- -moz-transform: rotate(-90deg);
- -ms-transform: rotate(-90deg);
- -o-transform: rotate(-90deg);
- transform: rotate(-90deg);
- /* also accepts left, right, top, bottom coordinates; not
- * required, but a good idea for styling */
- -webkit-transform-origin: 50% 50%;
- -moz-transform-origin: 50% 50%;
- -ms-transform-origin: 50% 50%;
- -o-transform-origin: 50% 50%;
- transform-origin: 50% 50%;
- /* Should be unset in IE9+ I think. */
- filter: progid:DXImageTransform.Microsoft.BasicImage(rotation=3);
- }
- /* The actual status box */
- .status div {
- display: block;
- background: rgb(0, 90, 156);
- color: white;
- width: 24em;
- padding-top: 0.3em;
- padding-left: 0em;
- padding-right: 5em;
- padding-bottom: 0.3em;
- /* Enable for debugging
- border: red thin solid;
- */
- }
- /* And text inside, don't confuse fonts as it breaks em above */
- .status div span {
- font-family: "Tauri";
- font-size: larger;
- }
|