diff options
-rwxr-xr-x | tools/makespec.py | 5 | ||||
-rw-r--r-- | tools/template.html | 15 |
2 files changed, 14 insertions, 6 deletions
diff --git a/tools/makespec.py b/tools/makespec.py index 925f23c..aa75b35 100755 --- a/tools/makespec.py +++ b/tools/makespec.py @@ -70,16 +70,17 @@ with open('spec.txt', 'r', encoding='utf-8') as spec: mdlines.append("<div class=\"examplenum\"><a href=\"#example-{0}\">Example {0}</a>".format(example)) if specformat == "html": mdlines.append(" <a class=\"dingus\" title=\"open in interactive dingus\">(interact)</a>") - mdlines.append("</div>\n\n") + mdlines.append("</div>\n<div class=\"column\">\n\n") mdlines.append("````````````````````````````````````````````````````````` markdown\n") stage = 1 elif stage == 1: mdlines.append("`````````````````````````````````````````````````````````\n\n") + mdlines.append("\n</div>\n\n<div class=\"column\">\n\n") mdlines.append("````````````````````````````````````````````````````````` html\n") stage = 2 elif stage == 2: mdlines.append("`````````````````````````````````````````````````````````\n\n") - mdlines.append("</div>\n") + mdlines.append("</div>\n</div>\n") stage = 0 else: sys.stderr.out("Encountered unknown stage {0}\n".format(stage)) diff --git a/tools/template.html b/tools/template.html index 39a196d..fd2e56b 100644 --- a/tools/template.html +++ b/tools/template.html @@ -39,9 +39,14 @@ pre { } code { font-family: monospace; background-color: #D3E1E4; } pre > code { background-color: transparent; } -div.example > pre { float:left; width: 48%; } -div.example > pre:nth-child(2) { clear:left; background-color: #D3E1E4; } -div.example > pre:nth-child(3) { clear:right; background-color: #C9CaCE; } +.example { font-size: 0; /* hack to get width:50% to work on inline-block */ + padding-bottom: 6pt; } +.column pre { font-size: 11pt; padding-left: 6pt; padding-right: 6pt; + padding-top: 2pt; padding-bottom: 2pt; } +div.examplenum { font-size: 11pt; text-align: left; } +div.column { display: inline-block; width: 50%; vertical-align: top; } +div.example > div:nth-child(2) { clear:left; background-color: #D3E1E4; } +div.example > div:nth-child(3) { clear:right; background-color: #C9CaCE; } #watermark { position:fixed; bottom:0px; @@ -54,7 +59,6 @@ div.example > pre:nth-child(3) { clear:right; background-color: #C9CaCE; } color: white; } #watermark a { color: white; } -div.examplenum { font-size: 82%; text-align: left; } a.dingus { color: red; cursor: pointer; } a.footnoteRef > sup:before { content: "["; @@ -76,6 +80,9 @@ a.footnoteRef > sup { line-height: 1.2; font-size: 10pt; } + .column pre { font-size: 9pt; } + div.examplenum { font-size: 9pt; } + a.dingus { display: none; } } </style> <script src="//code.jquery.com/jquery-1.11.0.min.js"></script> |