comparison src/tutorial.sml @ 1495:af0d4d11c5d7

Allow HTML in tutorial comments
author Adam Chlipala <adam@chlipala.net>
date Fri, 15 Jul 2011 17:25:09 -0400
parents 9ef6dd0df7a0
children 3010472edf44
comparison
equal deleted inserted replaced
1494:9ef6dd0df7a0 1495:af0d4d11c5d7
46 val outf = TextIO.openOut (OS.Path.mkAbsolute {relativeTo = OS.FileSys.getDir (), 46 val outf = TextIO.openOut (OS.Path.mkAbsolute {relativeTo = OS.FileSys.getDir (),
47 path = OS.Path.joinBaseExt {base = OS.Path.base fname, ext = SOME "html"}}) 47 path = OS.Path.joinBaseExt {base = OS.Path.base fname, ext = SOME "html"}})
48 48
49 val (befor, after) = Substring.position "<title>" source 49 val (befor, after) = Substring.position "<title>" source
50 50
51 fun proseLoop source =
52 let
53 val (befor, after) = Substring.splitl (fn ch => ch <> #"&") source
54 in
55 if Substring.isEmpty after then
56 TextIO.outputSubstr (outf, source)
57 else if Substring.size after >= 8 andalso Substring.string (Substring.slice (after, 1, SOME 7)) = "amp;lt;" then
58 (TextIO.outputSubstr (outf, befor);
59 TextIO.output (outf, "<");
60 proseLoop (Substring.slice (after, 8, NONE)))
61 else if Substring.size after >= 4 andalso Substring.string (Substring.slice (after, 1, SOME 3)) = "gt;" then
62 (TextIO.outputSubstr (outf, befor);
63 TextIO.output (outf, ">");
64 proseLoop (Substring.slice (after, 4, NONE)))
65 else if Substring.size after >= 5 andalso Substring.string (Substring.slice (after, 1, SOME 4)) = "amp;" then
66 (TextIO.outputSubstr (outf, befor);
67 TextIO.output (outf, "&");
68 proseLoop (Substring.slice (after, 5, NONE)))
69 else
70 raise Fail "Unsupported HTML escape"
71 end
72
51 fun loop source = 73 fun loop source =
52 let 74 let
53 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
54 in 76 in
55 if Substring.isEmpty after then 77 if Substring.isEmpty after then
62 if Substring.isEmpty after then 84 if Substring.isEmpty after then
63 TextIO.outputSubstr (outf, source) 85 TextIO.outputSubstr (outf, source)
64 else 86 else
65 (TextIO.outputSubstr (outf, befor); 87 (TextIO.outputSubstr (outf, befor);
66 TextIO.output (outf, "<div class=\"prose\">"); 88 TextIO.output (outf, "<div class=\"prose\">");
67 TextIO.outputSubstr (outf, befor'); 89 proseLoop befor';
68 TextIO.output (outf, "</div>"); 90 TextIO.output (outf, "</div>");
69 loop (Substring.slice (after, 49, NONE))) 91 loop (Substring.slice (after, 49, NONE)))
70 end 92 end
71 end 93 end
72 in 94 in