Admin/page/bin/mkcontents
author wenzelm
Sat, 12 Jan 2002 22:44:10 +0100
changeset 12732 c93b2f69b3ba
parent 9699 14dc0f812901
child 14490 7b37aa726d2d
permissions -rwxr-xr-x
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     1
#!/usr/bin/perl
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     2
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     3
# mkcontents.pl
8057
b15286c96788 ID line added
kleing
parents: 8056
diff changeset
     4
#
9699
14dc0f812901 fixed Id string
kleing
parents: 8057
diff changeset
     5
#   $Id$
8057
b15286c96788 ID line added
kleing
parents: 8056
diff changeset
     6
#
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     7
#   simple script to create a html version of the Contents file in the
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     8
#   Isabelle documentation directory.
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     9
#
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    10
#   Nov/14/1999 Version 1.0  -  Gerwin Klein <kleing@in.tum.de>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    11
#
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    12
#   command line:
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    13
#   mkcontent [-p <url-path-prefix>] <Content-file> <output-file>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    14
#
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    15
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    16
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    17
use Getopt::Long ;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    18
   
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    19
$opt_p="";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    20
$result = GetOptions ("p=s");
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    21
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    22
$path=$opt_p;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    23
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    24
$infile  = $ARGV[0];
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    25
$outfile = $ARGV[1];
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    26
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    27
$fileHeader = "<ul>\n";
12732
wenzelm
parents: 9699
diff changeset
    28
$lineHeader = "  <li>";
wenzelm
parents: 9699
diff changeset
    29
$lineEnd    = "</li>\n";
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    30
$fileFooter = "</ul>\n";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    31
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    32
open(IN, "<$infile") || die "cannot read input file <$infile>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    33
open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    34
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
print OUT $fileHeader;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    36
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
while (<IN>) {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    38
  if (/[ \t]*([^ \t]+)[ \t]+(.+)\n/) {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    39
    print OUT $lineHeader;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    40
    print OUT "<a href=\"$path$1.pdf\">$2</a>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    41
    print OUT $lineEnd;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    42
  }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    43
}
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    44
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    45
print OUT $fileFooter;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    46
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    47
close(OUT);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    48
close(IN);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    49
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    50
exit(0);