comparison src/tutorial.sml @ 1496:3010472edf44

Tutorial section headings
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 17:31:57 -0400
parents af0d4d11c5d7
children 0b639858200b
comparison
equal deleted inserted replaced
1495:af0d4d11c5d7 1496:3010472edf44
73 fun loop source = 73 fun loop source =
74 let 74 let
75 val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(* </span><span class=\"comment\">" source 75 val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(* </span><span class=\"comment\">" source
76 in 76 in
77 if Substring.isEmpty after then 77 if Substring.isEmpty after then
78 TextIO.outputSubstr (outf, source) 78 let
79 val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(** </span><span class=\"comment\">" source
80 in
81 if Substring.isEmpty after then
82 TextIO.outputSubstr (outf, source)
83 else
84 let
85 val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
86 (Substring.slice (after, 65, NONE))
87 in
88 if Substring.isEmpty after then
89 TextIO.outputSubstr (outf, source)
90 else
91 (TextIO.outputSubstr (outf, befor);
92 TextIO.output (outf, "<h2>");
93 proseLoop befor';
94 TextIO.output (outf, "</h2>");
95 loop (Substring.slice (after, 49, NONE)))
96 end
97 end
79 else 98 else
80 let 99 let
81 val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>" 100 val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
82 (Substring.slice (after, 64, NONE)) 101 (Substring.slice (after, 64, NONE))
83 in 102 in
102 TextIO.output (outf, "\t\tfont-family: Arial;\n"); 121 TextIO.output (outf, "\t\tfont-family: Arial;\n");
103 TextIO.output (outf, "\t\tbackground-color: #CCFFCC;\n"); 122 TextIO.output (outf, "\t\tbackground-color: #CCFFCC;\n");
104 TextIO.output (outf, "\t\tborder-style: solid;\n"); 123 TextIO.output (outf, "\t\tborder-style: solid;\n");
105 TextIO.output (outf, "\t\tpadding: 5px;\n"); 124 TextIO.output (outf, "\t\tpadding: 5px;\n");
106 TextIO.output (outf, "\t\tfont-size: larger;\n"); 125 TextIO.output (outf, "\t\tfont-size: larger;\n");
126 TextIO.output (outf, "\t}\n");
127 TextIO.output (outf, "\th2 {\n");
128 TextIO.output (outf, "\t\tfont-family: Arial;\n");
129 TextIO.output (outf, "\t\tfont-size: 20pt;\n");
130 TextIO.output (outf, "\t\tbackground-color: #99FF99;\n");
131 TextIO.output (outf, "\t\tpadding: 5px;\n");
107 TextIO.output (outf, "\t}\n"); 132 TextIO.output (outf, "\t}\n");
108 TextIO.output (outf, "-->\n"); 133 TextIO.output (outf, "-->\n");
109 TextIO.output (outf, "</style>\n"); 134 TextIO.output (outf, "</style>\n");
110 TextIO.output (outf, "<title>"); 135 TextIO.output (outf, "<title>");
111 TextIO.output (outf, title); 136 TextIO.output (outf, title);