blob: b17d28510acc85ee46a54be8b7e4d78d2422d3ab (
plain)
- <!DOCTYPE html>
- <html>
- <head>
- <meta charset="UTF-8">
- <title>$title$</title>
- <style type="text/css">
- body { font-family: Helvetica, arial, freesans, clean, sans-serif;
- line-height: 1.4;
- max-width: 48em;
- margin: auto;
- color: #333333;
- background-color: #fff;
- font-size: 13pt;
- }
- div#TOC ul { list-style: none; }
- h1 { font-size: 140%; font-weight: bold; border-top: 1px solid gray; padding-top: 0.5em; }
- h2 { font-size: 120%; font-weight: bold; }
- h3 { font-size: 110%; font-weight: bold; }
- h4 { font-size: 100%; font-weight: bold; }
- span.space { position: relative; }
- span.space:after {
- content: "";
- position: absolute;
- /* create a mark that indicates a space (trick from D. Greenspan) */
- top: 3px; bottom: 3px; left: 1px; right: 1px;
- border: 1px solid #999;
- }
- div.example { overflow: hidden; }
- p { text-align: justify; }
- pre { padding: 0.5em; margin-left: 0; margin-right: 0; margin-top: 0.2em;
- margin-bottom: 0.5em; font-size: 88%; }
- pre {
- white-space: pre-wrap; /* css-3 */
- white-space: -moz-pre-wrap; /* Mozilla, since 1999 */
- white-space: -pre-wrap; /* Opera 4-6 */
- white-space: -o-pre-wrap; /* Opera 7 */
- word-wrap: break-word; /* Internet Explorer 5.5+ */
- }
- code { font-family: monospace; background-color: #D3E1E4; }
- pre > code { background-color: transparent; }
- div.example > pre { float:left; width: 48%; }
- div.example > pre.markdown { clear:left; }
- pre.tree { font-weight: bold; color: #777; }
- pre.markdown { background-color: #D3E1E4; }
- pre.html { background-color: #C9CaCE; }
- pre.html span.space:after {
- border: 1px solid #666;
- }
- div.examplenum { font-size: 82%; text-align: left; }
- a.dingus { color: red; }
- a.footnoteRef > sup:before {
- content: "[";
- }
- a.footnoteRef > sup:after {
- content: "]";
- }
- a.footnoteRef > sup {
- vertical-align: baseline;
- font-size: 100%;
- }
- </style>
- <script src="//code.jquery.com/jquery-1.11.0.min.js"></script>
- <script type="text/javascript">
- $$(document).ready(function() {
- $$("div.example").each(function(e) {
- var t = $$(this).find('pre.markdown > code').text();
- $$(this).find('a.dingus').click(function(f) {
- window.open('/dingus.html?text=' + encodeURIComponent(t));
- });
- });
- $$("pre.markdown").dblclick(function(e) { window.open('/dingus.html?text=' +
- encodeURIComponent($$(this).find('code').text()));
- });
- });
- </script>
- </head>
- <body>
- $if(title)$
- <h1 class="title">$title$</h1>
- $endif$
- $if(version)$
- <div class="version">Version $version$ ($date$)</div>
- $endif$
- <div class="authors">
- $for(author)$<span class="author">$author$</span>$sep$; $endfor$
- </div>
- <div id="TOC">
- $toc$
- </div>
- $body$
- </body>
- </html>
|