summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:25:09 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-07-15 17:25:09 -0400
commit76a1338e6d9b75a03c7741f2c0df827043c97b34 (patch)
tree7e42609843840dee056822c9068c7b5758196e1f /src
parent486c4f75cb34e0c9aa4069fda1595c722da38d07 (diff)
Allow HTML in tutorial comments
Diffstat (limited to 'src')
-rw-r--r--src/tutorial.sml24
1 files changed, 23 insertions, 1 deletions
diff --git a/src/tutorial.sml b/src/tutorial.sml
index 84244197..2b875c0b 100644
--- a/src/tutorial.sml
+++ b/src/tutorial.sml
@@ -48,6 +48,28 @@ fun fixupFile (fname, title) =
val (befor, after) = Substring.position "<title>" source
+ fun proseLoop source =
+ let
+ val (befor, after) = Substring.splitl (fn ch => ch <> #"&") source
+ in
+ if Substring.isEmpty after then
+ TextIO.outputSubstr (outf, source)
+ else if Substring.size after >= 8 andalso Substring.string (Substring.slice (after, 1, SOME 7)) = "amp;lt;" then
+ (TextIO.outputSubstr (outf, befor);
+ TextIO.output (outf, "<");
+ proseLoop (Substring.slice (after, 8, NONE)))
+ else if Substring.size after >= 4 andalso Substring.string (Substring.slice (after, 1, SOME 3)) = "gt;" then
+ (TextIO.outputSubstr (outf, befor);
+ TextIO.output (outf, ">");
+ proseLoop (Substring.slice (after, 4, NONE)))
+ else if Substring.size after >= 5 andalso Substring.string (Substring.slice (after, 1, SOME 4)) = "amp;" then
+ (TextIO.outputSubstr (outf, befor);
+ TextIO.output (outf, "&");
+ proseLoop (Substring.slice (after, 5, NONE)))
+ else
+ raise Fail "Unsupported HTML escape"
+ end
+
fun loop source =
let
val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(* </span><span class=\"comment\">" source
@@ -64,7 +86,7 @@ fun fixupFile (fname, title) =
else
(TextIO.outputSubstr (outf, befor);
TextIO.output (outf, "<div class=\"prose\">");
- TextIO.outputSubstr (outf, befor');
+ proseLoop befor';
TextIO.output (outf, "</div>");
loop (Substring.slice (after, 49, NONE)))
end