8056
|
1 |
#!/usr/bin/perl
|
|
2 |
|
|
3 |
# mkcontents.pl
|
8057
|
4 |
#
|
|
5 |
# $ID$
|
|
6 |
#
|
8056
|
7 |
# simple script to create a html version of the Contents file in the
|
|
8 |
# Isabelle documentation directory.
|
|
9 |
#
|
|
10 |
# Nov/14/1999 Version 1.0 - Gerwin Klein <kleing@in.tum.de>
|
|
11 |
#
|
|
12 |
# command line:
|
|
13 |
# mkcontent [-p <url-path-prefix>] <Content-file> <output-file>
|
|
14 |
#
|
|
15 |
|
|
16 |
|
|
17 |
use Getopt::Long ;
|
|
18 |
|
|
19 |
$opt_p="";
|
|
20 |
$result = GetOptions ("p=s");
|
|
21 |
|
|
22 |
$path=$opt_p;
|
|
23 |
|
|
24 |
$infile = $ARGV[0];
|
|
25 |
$outfile = $ARGV[1];
|
|
26 |
|
|
27 |
$fileHeader = "<ul>\n";
|
|
28 |
$lineHeader = " <li> ";
|
|
29 |
$lineEnd = " </li>\n";
|
|
30 |
$fileFooter = "</ul>\n";
|
|
31 |
|
|
32 |
open(IN, "<$infile") || die "cannot read input file <$infile>";
|
|
33 |
open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
|
|
34 |
|
|
35 |
print OUT $fileHeader;
|
|
36 |
|
|
37 |
while (<IN>) {
|
|
38 |
if (/[ \t]*([^ \t]+)[ \t]+(.+)\n/) {
|
|
39 |
print OUT $lineHeader;
|
|
40 |
print OUT "<a href=\"$path$1.pdf\">$2</a>";
|
|
41 |
print OUT $lineEnd;
|
|
42 |
}
|
|
43 |
}
|
|
44 |
|
|
45 |
print OUT $fileFooter;
|
|
46 |
|
|
47 |
close(OUT);
|
|
48 |
close(IN);
|
|
49 |
|
|
50 |
exit(0);
|