Mercurial > urweb

annotate src/tutorial.sml @ 2219:ff38b3e0cdfd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add interface to UnionFind.
author Ziv Scully <ziv@mit.edu>
date Mon, 24 Nov 2014 20:41:24 -0500
parents 2d9f831d45c9
children
rev   line source
adam@1493 1 (* Copyright (c) 2011, Adam Chlipala
adam@1493 2 * All rights reserved.
adam@1493 3 *
adam@1493 4 * Redistribution and use in source and binary forms, with or without
adam@1493 5 * modification, are permitted provided that the following conditions are met:
adam@1493 6 *
adam@1493 7 * - Redistributions of source code must retain the above copyright notice,
adam@1493 8 * this list of conditions and the following disclaimer.
adam@1493 9 * - Redistributions in binary form must reproduce the above copyright notice,
adam@1493 10 * this list of conditions and the following disclaimer in the documentation
adam@1493 11 * and/or other materials provided with the distribution.
adam@1493 12 * - The names of contributors may not be used to endorse or promote products
adam@1493 13 * derived from this software without specific prior written permission.
adam@1493 14 *
adam@1493 15 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adam@1493 16 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adam@1493 17 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adam@1493 18 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adam@1493 19 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
adam@1493 20 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adam@1493 21 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adam@1493 22 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adam@1493 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adam@1493 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adam@1493 25 * POSSIBILITY OF SUCH DAMAGE.
adam@1493 26 *)
adam@1493 27
adam@1493 28 structure Tutorial :> TUTORIAL = struct
adam@1493 29
adam@1494 30 fun readAll inf =
adam@1493 31 let
adam@1493 32 fun loop acc =
adam@1493 33 case TextIO.inputLine inf of
adam@1493 34 NONE => Substring.full (String.concat (rev acc))
adam@1493 35 | SOME line => loop (line :: acc)
adam@1493 36 in
adam@1493 37 loop []
adam@1493 38 before TextIO.closeIn inf
adam@1493 39 end
adam@1493 40
adam@1494 41 val readAllFile = readAll o TextIO.openIn
adam@1494 42
adam@1494 43 fun fixupFile (fname, title) =
adam@1494 44 let
adam@1494 45 val source = readAllFile "/tmp/final.html"
adam@1494 46 val outf = TextIO.openOut (OS.Path.mkAbsolute {relativeTo = OS.FileSys.getDir (),
adam@1494 47 path = OS.Path.joinBaseExt {base = OS.Path.base fname, ext = SOME "html"}})
adam@1494 48
adam@1494 49 val (befor, after) = Substring.position "<title>" source
adam@1494 50
adam@1495 51 fun proseLoop source =
adam@1495 52 let
adam@1495 53 val (befor, after) = Substring.splitl (fn ch => ch <> #"&") source
adam@1495 54 in
adam@1495 55 if Substring.isEmpty after then
adam@1495 56 TextIO.outputSubstr (outf, source)
adam@1497 57 else if Substring.size after >= 4 andalso Substring.string (Substring.slice (after, 1, SOME 3)) = "lt;" then
adam@1495 58 (TextIO.outputSubstr (outf, befor);
adam@1495 59 TextIO.output (outf, "<");
adam@1497 60 proseLoop (Substring.slice (after, 4, NONE)))
adam@1495 61 else if Substring.size after >= 4 andalso Substring.string (Substring.slice (after, 1, SOME 3)) = "gt;" then
adam@1495 62 (TextIO.outputSubstr (outf, befor);
adam@1495 63 TextIO.output (outf, ">");
adam@1495 64 proseLoop (Substring.slice (after, 4, NONE)))
adam@1495 65 else if Substring.size after >= 5 andalso Substring.string (Substring.slice (after, 1, SOME 4)) = "amp;" then
adam@1495 66 (TextIO.outputSubstr (outf, befor);
adam@1495 67 TextIO.output (outf, "&");
adam@1495 68 proseLoop (Substring.slice (after, 5, NONE)))
adam@1495 69 else
adam@1495 70 raise Fail "Unsupported HTML escape"
adam@1495 71 end
adam@1495 72
adam@1494 73 fun loop source =
adam@1494 74 let
adam@1494 75 val (befor, after) = Substring.position "<span class=\"comment-delimiter\">(* </span><span class=\"comment\">" source
adam@1494 76 in
adam@1494 77 if Substring.isEmpty after then
adam@1497 78 TextIO.outputSubstr (outf, source)
adam@1494 79 else
adam@1494 80 let
adam@1494 81 val (befor', after) = Substring.position " </span><span class=\"comment-delimiter\">*)</span>"
adam@1498 82 (Substring.slice (after, 64, NONE))
adam@1494 83 in
adam@1494 84 if Substring.isEmpty after then
adam@1494 85 TextIO.outputSubstr (outf, source)
adam@1494 86 else
adam@1494 87 (TextIO.outputSubstr (outf, befor);
adam@1497 88 TextIO.output (outf, "</pre>");
adam@1497 89 if Substring.size befor' >= 1 andalso Substring.sub (befor', 0) = #"*" then
adam@1497 90 (TextIO.output (outf, "<h2>");
adam@1497 91 proseLoop (Substring.slice (befor', 2, NONE));
adam@1497 92 TextIO.output (outf, "</h2>"))
adam@1497 93 else
adam@1497 94 (TextIO.output (outf, "<div class=\"prose\">");
adam@1497 95 proseLoop befor';
adam@1497 96 TextIO.output (outf, "</div>"));
adam@1497 97 TextIO.output (outf, "<pre>");
adam@1494 98 loop (Substring.slice (after, 49, NONE)))
adam@1494 99 end
adam@1494 100 end
adam@1494 101 in
adam@1494 102 if Substring.isEmpty after then
adam@1494 103 raise Fail ("Missing <title> for " ^ title)
adam@1494 104 else
adam@1494 105 (TextIO.outputSubstr (outf, befor);
adam@1494 106 TextIO.output (outf, "<style type=\"text/css\">\n");
adam@1494 107 TextIO.output (outf, "<!--\n");
adam@1494 108 TextIO.output (outf, "\tdiv.prose {\n");
adam@1494 109 TextIO.output (outf, "\t\tfont-family: Arial;\n");
adam@1494 110 TextIO.output (outf, "\t\tbackground-color: #CCFFCC;\n");
adam@1494 111 TextIO.output (outf, "\t\tborder-style: solid;\n");
adam@1494 112 TextIO.output (outf, "\t\tpadding: 5px;\n");
adam@1494 113 TextIO.output (outf, "\t\tfont-size: larger;\n");
adam@1494 114 TextIO.output (outf, "\t}\n");
adam@1496 115 TextIO.output (outf, "\th2 {\n");
adam@1496 116 TextIO.output (outf, "\t\tfont-family: Arial;\n");
adam@1496 117 TextIO.output (outf, "\t\tfont-size: 20pt;\n");
adam@1496 118 TextIO.output (outf, "\t\tbackground-color: #99FF99;\n");
adam@1496 119 TextIO.output (outf, "\t\tpadding: 5px;\n");
adam@1496 120 TextIO.output (outf, "\t}\n");
adam@1497 121 TextIO.output (outf, "\ta:link {\n");
adam@1497 122 TextIO.output (outf, "\t\ttext-decoration: underline;\n");
adam@1497 123 TextIO.output (outf, "\t\tcolor: blue;\n");
adam@1497 124 TextIO.output (outf, "\t}\n");
adam@1497 125 TextIO.output (outf, "\ta:visited {\n");
adam@1497 126 TextIO.output (outf, "\t\ttext-decoration: underline;\n");
adam@1497 127 TextIO.output (outf, "\t\tcolor: red;\n");
adam@1497 128 TextIO.output (outf, "\t}\n");
adam@1494 129 TextIO.output (outf, "-->\n");
adam@1494 130 TextIO.output (outf, "</style>\n");
adam@1494 131 TextIO.output (outf, "<title>");
adam@1494 132 TextIO.output (outf, title);
adam@1494 133 let
adam@1494 134 val (befor, after) = Substring.position "</title>" after
adam@1494 135 in
adam@1494 136 if Substring.isEmpty after then
adam@1494 137 raise Fail ("Missing </title> for " ^ title)
adam@1494 138 else
adam@1494 139 let
adam@1494 140 val (befor, after) = Substring.position "<body>" after
adam@1494 141 in
adam@1494 142 if Substring.isEmpty after then
adam@1494 143 raise Fail ("Missing <body> for " ^ title)
adam@1494 144 else
adam@1494 145 (TextIO.outputSubstr (outf, befor);
adam@1494 146 TextIO.output (outf, "<body><h1>");
adam@1494 147 TextIO.output (outf, title);
adam@1494 148 TextIO.output (outf, "</h1>");
adam@1494 149 loop (Substring.slice (after, 6, NONE)))
adam@1494 150 end
adam@1494 151 end;
adam@1494 152 TextIO.closeOut outf)
adam@1494 153 end
adam@1493 154
adam@1493 155 fun doUr fname =
adam@1493 156 let
adam@1494 157 val inf = TextIO.openIn fname
adam@1494 158
adam@1494 159 val title = case TextIO.inputLine inf of
adam@1494 160 NONE => raise Fail ("No title comment at start of " ^ fname)
adam@1494 161 | SOME title => title
adam@1494 162
adam@1494 163 val title = String.substring (title, 3, size title - 7)
adam@1494 164
adam@1493 165 val eval = TextIO.openOut "/tmp/eval.ur"
adam@1493 166 val gen = TextIO.openOut "/tmp/gen.ur"
adam@1493 167
adam@1493 168 fun untilEnd source =
adam@1493 169 let
adam@1493 170 val (befor, after) = Substring.position "(* end *)" source
adam@1493 171 in
adam@1493 172 if Substring.isEmpty after then
adam@1493 173 (source, Substring.full "")
adam@1493 174 else
adam@1493 175 (befor, Substring.slice (after, 9, NONE))
adam@1493 176 end
adam@1493 177
adam@1493 178 fun doDirectives (count, source) =
adam@1493 179 let
adam@1493 180 val safe = String.translate (fn #"<" => "&lt;"
adam@1493 181 | #"&" => "&amp;"
adam@1493 182 | #"{" => "&#123;"
adam@1493 183 | #"(" => "&#40;"
adam@1493 184 | #"\n" => "&#40;*NL*)\n"
adam@1499 185 | #" " => "&#40;*NL*) "
adam@1493 186 | ch => str ch) o Substring.string
adam@1493 187
adam@1493 188 val (befor, after) = Substring.position "(* begin " source
adam@1493 189
adam@1493 190 fun default () = (TextIO.outputSubstr (eval, source);
adam@1493 191 TextIO.output (gen, safe source))
adam@1493 192 in
adam@1493 193 if Substring.isEmpty after then
adam@1493 194 default ()
adam@1493 195 else
adam@1493 196 let
adam@1493 197 val (command, after) = Substring.splitl (not o Char.isSpace) (Substring.slice (after, 9, NONE))
adam@1493 198 in
adam@1493 199 if Substring.isEmpty after then
adam@1493 200 default ()
adam@1493 201 else
adam@1493 202 let
adam@1493 203 val (_, rest) = Substring.position "*)" after
adam@1493 204 in
adam@1493 205 if Substring.isEmpty rest then
adam@1493 206 default ()
adam@1493 207 else
adam@1493 208 let
adam@1493 209 val (arg, source) = untilEnd (Substring.slice (rest, 3, NONE))
adam@1493 210 val () = (TextIO.outputSubstr (eval, befor);
adam@1493 211 TextIO.output (gen, safe befor))
adam@1493 212 val (count, skip) =
adam@1493 213 case Substring.string command of
adam@1493 214 "hide" => (TextIO.outputSubstr (eval, arg);
adam@1493 215 (count, true))
adam@1493 216 | "eval" => (TextIO.output (eval, "val _eval");
adam@1493 217 TextIO.output (eval, Int.toString count);
adam@1493 218 TextIO.output (eval, " = ");
adam@1493 219 TextIO.outputSubstr (eval, arg);
adam@1493 220 TextIO.output (eval, "\n\n");
adam@1493 221
adam@1493 222 TextIO.output (gen, safe arg);
adam@1493 223 TextIO.output (gen, "== {[_eval");
adam@1493 224 TextIO.output (gen, Int.toString count);
adam@1493 225 TextIO.output (gen, "]}");
adam@1493 226
adam@1493 227 (count + 1, false))
adam@1493 228 | s => raise Fail ("Unknown tutorial directive: " ^ s)
adam@1493 229 in
adam@1493 230 doDirectives (count, if skip then
adam@1493 231 #2 (Substring.splitl Char.isSpace source)
adam@1493 232 else
adam@1493 233 source)
adam@1493 234 end
adam@1493 235 end
adam@1493 236 end
adam@1493 237 end
adam@1493 238 in
adam@1494 239 doDirectives (0, readAll inf);
adam@1493 240 TextIO.closeOut gen;
adam@1493 241
adam@1493 242 TextIO.output (eval, "\n\nfun main () : transaction page =\nreturn <xml><body>");
adam@1494 243 TextIO.outputSubstr (eval, readAllFile "/tmp/gen.ur");
adam@1493 244 TextIO.output (eval, "</body></xml>");
adam@1493 245 TextIO.closeOut eval;
adam@1493 246
adam@1493 247 if Compiler.compile "/tmp/eval" then
adam@1493 248 let
adam@1493 249 val proc = Unix.execute ("/bin/sh", ["-c", "/tmp/eval.exe /main"])
adam@1493 250 val inf = Unix.textInstreamOf proc
adam@1494 251 val s = readAll inf
adam@1493 252 val _ = Unix.reap proc
adam@1493 253
adam@1814 254 val (befor, after) = Substring.position "<body>" s
adam@1493 255 in
adam@1493 256 if Substring.isEmpty after then
adam@1493 257 print ("Bad output for " ^ fname ^ "! [1]\n")
adam@1493 258 else
adam@1493 259 let
adam@1814 260 val after = Substring.slice (after, 6, NONE)
adam@1493 261 val (befor, after) = Substring.position "</body>" after
adam@1493 262 in
adam@1493 263 if Substring.isEmpty after then
adam@1493 264 print ("Bad output for " ^ fname ^ "! [2]\n")
adam@1493 265 else
adam@1493 266 let
adam@1493 267 val outf = TextIO.openOut "/tmp/final.ur"
adam@1493 268
adam@1493 269 fun eatNls source =
adam@1493 270 let
adam@1493 271 val (befor, after) = Substring.position "(*NL*)" source
adam@1493 272 in
adam@1493 273 if Substring.isEmpty after then
adam@1493 274 TextIO.outputSubstr (outf, source)
adam@1493 275 else
adam@1493 276 (TextIO.outputSubstr (outf, befor);
adam@1493 277 eatNls (Substring.slice (after, 6, NONE)))
adam@1493 278 end
adam@1493 279
adam@1493 280 val cmd = "emacs --eval \"(progn "
adam@1493 281 ^ "(global-font-lock-mode t) "
adam@1493 282 ^ "(add-to-list 'load-path \\\""
ezyang@1739 283 ^ !Settings.configSitelisp
adam@1493 284 ^ "/\\\") "
adam@1493 285 ^ "(load \\\"urweb-mode-startup\\\") "
adam@1493 286 ^ "(urweb-mode) "
adam@1497 287 ^ "(find-file \\\"/tmp/final2.ur\\\") "
adam@1493 288 ^ "(switch-to-buffer (htmlize-buffer)) "
adam@1494 289 ^ "(write-file \\\"/tmp/final.html\\\") "
adam@1493 290 ^ "(kill-emacs))\""
adam@1493 291 in
adam@1493 292 eatNls befor;
adam@1493 293 TextIO.closeOut outf;
adam@1497 294 ignore (OS.Process.system "sed -e 's/&lt;/</g;s/&amp;/\\&/g' </tmp/final.ur >/tmp/final2.ur");
adam@1494 295 ignore (OS.Process.system cmd);
adam@1494 296 fixupFile (fname, title)
adam@1493 297 end
adam@1493 298 end
adam@1493 299 end
adam@1493 300 else
adam@1493 301 ()
adam@1493 302 end
adam@1493 303
adam@1493 304 fun make dirname =
adam@1493 305 let
adam@1493 306 val dir = OS.FileSys.openDir dirname
adam@1493 307
adam@1493 308 fun doDir () =
adam@1493 309 case OS.FileSys.readDir dir of
adam@1493 310 NONE => OS.FileSys.closeDir dir
adam@1493 311 | SOME fname =>
adam@1493 312 (if OS.Path.ext fname = SOME "ur" then
adam@1493 313 doUr (OS.Path.joinDirFile {dir = dirname, file = fname})
adam@1493 314 else
adam@1493 315 ();
adam@1493 316 doDir ())
adam@1493 317 in
adam@1493 318 Settings.setProtocol "static";
adam@1493 319 doDir ()
adam@1493 320 end
adam@1493 321
adam@1493 322 end