diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-19 14:53:38 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-19 14:53:38 -0400 |
| commit | 6b4491e84c22056a9d97c34abc9c3561108f2497 (patch) | |
| tree | 66774c341750105164edb53e349eca4b2409e6db /src | |
| parent | b540e401c63dfc5e5472be2869d93027b1dfc6a4 (diff) | |
Small demo prettifications
Diffstat (limited to 'src')
| -rw-r--r-- | src/demo.sml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/src/demo.sml b/src/demo.sml index 1e448660..015090e0 100644 --- a/src/demo.sml +++ b/src/demo.sml @@ -112,7 +112,7 @@ fun make {prefix, dirname} = file = out} val out = TextIO.openOut out - val () = (TextIO.output (out, "<frameset rows=\"75%,25%\">\n"); + val () = (TextIO.output (out, "<frameset rows=\"50%,*\">\n"); TextIO.output (out, "<frame src=\""); TextIO.output (out, prefix); TextIO.output (out, "/"); @@ -287,11 +287,7 @@ fun make {prefix, dirname} = | 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>"); + TextIO.output (out, "<html><body>\n\n<pre>"); loop (); TextIO.output (out, "</pre>\n\n</body></html>"); |