diff src/demo.sml @ 381:1fe85b58c9ba

Generating urp HTML
author Adam Chlipala <adamc@hcoop.net>
date Sun, 19 Oct 2008 14:13:08 -0400
parents 758304561b60
children aa2edbd47041
line wrap: on
line diff
--- a/src/demo.sml	Sun Oct 19 14:05:00 2008 -0400
+++ b/src/demo.sml	Sun Oct 19 14:13:08 2008 -0400
@@ -47,7 +47,7 @@
                                          file = "index.html"}
 
         val out = TextIO.openOut fname
-        val () = (TextIO.output (out, "<frameset cols=\"15%,90%\">\n");
+        val () = (TextIO.output (out, "<frameset cols=\"10%,90%\">\n");
                   TextIO.output (out, "<frame src=\"demos.html\">\n");
                   TextIO.output (out, "<frame src=\"intro.html\" name=\"staging\">\n");
                   TextIO.output (out, "</frameset>\n");
@@ -57,7 +57,7 @@
                                          file = "demos.html"}
 
         val demosOut = TextIO.openOut fname
-        val () = (TextIO.output (demosOut, "<html><body><ul>\n\n");
+        val () = (TextIO.output (demosOut, "<html><body>\n\n");
                   TextIO.output (demosOut, "<li> <a target=\"staging\" href=\"intro.html\">Intro</a></li>\n\n"))
 
         fun mergeWith f (o1, o2) =
@@ -227,11 +227,60 @@
                         (TextIO.output (out, line);
                          readIndex ())
             end
+
+        fun prettyPrint () =
+            let
+                val dir = Posix.FileSys.opendir dirname
+
+                fun loop () =
+                    case Posix.FileSys.readdir dir of
+                        NONE => Posix.FileSys.closedir dir
+                      | SOME file =>
+                        let
+                            fun doit f =
+                                f (OS.Path.joinDirFile {dir = dirname,
+                                                        file = file},
+                                   OS.Path.joinDirFile {dir = outDir,
+                                                        file = OS.Path.joinBaseExt {base = file,
+                                                                                    ext = SOME "html"}})
+                        in
+                            case OS.Path.ext file of
+                                SOME "urp" =>
+                                doit (fn (src, html) =>
+                                         let
+                                             val inf = TextIO.openIn src
+                                             val out = TextIO.openOut html
+
+                                             fun loop () =
+                                                 case TextIO.inputLine inf of
+                                                     NONE => ()
+                                                   | SOME line => (TextIO.output (out, line);
+                                                                   loop ())
+                                         in
+                                             TextIO.output (out, "<html><head>\n<title>");
+                                             TextIO.output (out, file);
+                                             TextIO.output (out, "</title>\n</head><body>\n<h1>");
+                                             TextIO.output (out, file);
+                                             TextIO.output (out, "</h1>\n\n<pre>");
+                                             loop ();
+                                             TextIO.output (out, "</pre>\n\n</body></html>");
+
+                                             TextIO.closeIn inf;
+                                             TextIO.closeOut out
+                                         end)
+                              | _ => ();
+                            loop ()
+                        end
+            in
+                loop ()
+            end
     in
         readIndex ();
 
-        TextIO.output (demosOut, "\n</ul></body></html>\n");
-        TextIO.closeOut demosOut
+        TextIO.output (demosOut, "\n</body></html>\n");
+        TextIO.closeOut demosOut;
+
+        prettyPrint ()
     end
 
 end