1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
#!/bin/sh
set -e
name=`basename $0`
dir=`dirname $0`
src=`cd $dir/.. && pwd`
bin="$src/bin"
die () {
echo >&2 "$1"
exit 1
}
usage () {
die "usage: $name"
}
case "$#" in
0)
;;
*)
usage
;;
esac
book='mlton.book'
pages='.pages'
pdf='mlton-guide.pdf'
script='.script'
titlepage='title.html'
tmp="/tmp/mlton-guide.$$"
version=`date +%Y%m%d`
rm -rf $tmp
mkdir $tmp
cd $tmp
( cd $src/doc/guide && tar -cf - . ) | tar -xf -
# The grep -v takes out files that aren't wiki pages.
ls -1 | grep -v '\.' >$pages
echo 'Massaging HTML.'
for f in `cat $pages`; do
cat >$script <<EOF
/^<table bgcolor = lightblue/,+29d
s;\(<body .*\);\1\n<h1>$f</h1>;
s;<FONT[^>]*>;;g
s;</FONT>;;g
s;\(<div id="content"\);\1;
s;<td colspan = 3;<td align = right;
s;<img src=\"\(http://mlton.org[^>]*\)>;<img src="moin-www.png"><a href=\"\1>image</a>;g
EOF
$bin/msed -f $script <$f >.tmp
mv .tmp $f
done
echo 'Generating PDF titlepage.'
cat >$titlepage <<EOF
<html>
<head><title>MLton Guide ($version)</title></head>
<body>
<h1>MLton Guide</h1>
<p>
This is the guide for MLton, an open-source, whole-program,
optimizing Standard ML compiler.
</p>
<p>
This guide was generated automatically from the MLton wiki,
available online at <a href="http://mlton.org/">http://mlton.org</a>.
It is up to date for MLton $version.
</p>
</body>
</html>
EOF
echo 'Generating htmldoc script.'
(
cat <<EOF
#HTMLDOC 1.8.24 Open Source
-f $pdf
-t pdf13
--bodyfont times
--bottom 0.50in
--browserwidth 680
--charset iso-8859-1
--color
--compression=9
--effectduration 1.0
--embedfonts
--firstpage p1
--fontsize 11.0
--fontspacing 1.2
--footer ..1
--header t.c
--headfootfont Helvetica
--headfootsize 11.0
--headingfont Helvetica
--jpeg=0
--left 1.00in
--links
--linkstyle underline
--no-encryption
--no-pscommands
--no-strict
--no-xrxcomments
--nup 1
--pageduration 10
--pageeffect none
--pagelayout single
--pagemode document
--portrait
--right 0.50in
--size Universal
--title
--top 0.50in
--webpage
$titlepage
Home
Index
EOF
grep -v '^\(Home\|Index\)$' $pages
) >$book
echo 'Running htmldoc.'
htmldoc --batch $book || true
mv $pdf $src/doc/guide
rm -rf $tmp
|
