summaryrefslogtreecommitdiff
path: root/src/tutorial.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:31:57 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:31:57 -0400
commitb36a8def513d0fdd96fce220cf1f14409853c7b5 (patch)
tree9e916c08f89e01ce4d2dfb17dea9ddc2e730b649 /src/tutorial.sml
parent76a1338e6d9b75a03c7741f2c0df827043c97b34 (diff)
Tutorial section headings
Diffstat (limited to 'src/tutorial.sml')
-rw-r--r--src/tutorial.sml27
1 files changed, 26 insertions, 1 deletions
diff --git a/src/tutorial.sml b/src/tutorial.sml
index 2b875c0b..a2156adc 100644
--- a/src/tutorial.sml
+++ b/src/tutorial.sml
@@ -75,7 +75,26 @@ fun fixupFile (fname, title) =
val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(* </span><span class=\"comment\">" source
in
if Substring.isEmpty after then
- TextIO.outputSubstr (outf, source)
+ let
+ val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(** </span><span class=\"comment\">" source
+ in
+ if Substring.isEmpty after then
+ TextIO.outputSubstr (outf, source)
+ else
+ let
+ val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
+ (Substring.slice (after, 65, NONE))
+ in
+ if Substring.isEmpty after then
+ TextIO.outputSubstr (outf, source)
+ else
+ (TextIO.outputSubstr (outf, befor);
+ TextIO.output (outf, "<h2>");
+ proseLoop befor';
+ TextIO.output (outf, "</h2>");
+ loop (Substring.slice (after, 49, NONE)))
+ end
+ end
else
let
val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
@@ -105,6 +124,12 @@ fun fixupFile (fname, title) =
TextIO.output (outf, "\t\tpadding: 5px;\n");
TextIO.output (outf, "\t\tfont-size: larger;\n");
TextIO.output (outf, "\t}\n");
+ TextIO.output (outf, "\th2 {\n");
+ TextIO.output (outf, "\t\tfont-family: Arial;\n");
+ TextIO.output (outf, "\t\tfont-size: 20pt;\n");
+ TextIO.output (outf, "\t\tbackground-color: #99FF99;\n");
+ TextIO.output (outf, "\t\tpadding: 5px;\n");
+ TextIO.output (outf, "\t}\n");
TextIO.output (outf, "-->\n");
TextIO.output (outf, "</style>\n");
TextIO.output (outf, "<title>");