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