Admin/website/build/mkcontents.pl
author haftmann
Sat, 04 Jun 2005 10:26:08 +0200
changeset 16233 e634d33deb86
permissions -rwxr-xr-x
added new website
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16233
e634d33deb86 added new website
haftmann
parents:
diff changeset
     1
#!/usr/bin/perl
e634d33deb86 added new website
haftmann
parents:
diff changeset
     2
e634d33deb86 added new website
haftmann
parents:
diff changeset
     3
# mkcontents.pl
e634d33deb86 added new website
haftmann
parents:
diff changeset
     4
#
e634d33deb86 added new website
haftmann
parents:
diff changeset
     5
#   $Id$
e634d33deb86 added new website
haftmann
parents:
diff changeset
     6
#
e634d33deb86 added new website
haftmann
parents:
diff changeset
     7
#   simple script to create a html version of the Contents file in the
e634d33deb86 added new website
haftmann
parents:
diff changeset
     8
#   Isabelle documentation directory.
e634d33deb86 added new website
haftmann
parents:
diff changeset
     9
#
e634d33deb86 added new website
haftmann
parents:
diff changeset
    10
#   Nov/14/1999 Version 1.0  -  Gerwin Klein <kleing@in.tum.de>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    11
#
e634d33deb86 added new website
haftmann
parents:
diff changeset
    12
#   command line:
e634d33deb86 added new website
haftmann
parents:
diff changeset
    13
#   mkcontent.pl [-p <url-path-prefix>] <Content-file> <output-file>
e634d33deb86 added new website
haftmann
parents:
diff changeset
    14
#
e634d33deb86 added new website
haftmann
parents:
diff changeset
    15
e634d33deb86 added new website
haftmann
parents:
diff changeset
    16
e634d33deb86 added new website
haftmann
parents:
diff changeset
    17
use Getopt::Long ;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    18
e634d33deb86 added new website
haftmann
parents:
diff changeset
    19
$opt_p="";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    20
$result = GetOptions ("p=s");
e634d33deb86 added new website
haftmann
parents:
diff changeset
    21
e634d33deb86 added new website
haftmann
parents:
diff changeset
    22
$path=$opt_p;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    23
e634d33deb86 added new website
haftmann
parents:
diff changeset
    24
$infile  = $ARGV[0];
e634d33deb86 added new website
haftmann
parents:
diff changeset
    25
$outfile = $ARGV[1];
e634d33deb86 added new website
haftmann
parents:
diff changeset
    26
e634d33deb86 added new website
haftmann
parents:
diff changeset
    27
$listHeader = "<ul>\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    28
$lineHeader = "  <li>";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    29
$lineEnd    = "</li>\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    30
$listFooter = "</ul>\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    31
e634d33deb86 added new website
haftmann
parents:
diff changeset
    32
$topicStart = "<h3>";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    33
$topicEnd   = "</h3>\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    34
e634d33deb86 added new website
haftmann
parents:
diff changeset
    35
open(IN, "<$infile") || die "cannot read input file <$infile>";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    36
open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    37
e634d33deb86 added new website
haftmann
parents:
diff changeset
    38
$first = 1;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    39
e634d33deb86 added new website
haftmann
parents:
diff changeset
    40
print OUT '<?xml version="1.0" encoding="iso-8859-1" ?>' . "\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    41
print OUT '<dummy:wrapper xmlns:dummy="http://nowhere.no">' . "\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    42
e634d33deb86 added new website
haftmann
parents:
diff changeset
    43
while (<IN>) {
e634d33deb86 added new website
haftmann
parents:
diff changeset
    44
  if (/^([^ \t].*)\n/) {
e634d33deb86 added new website
haftmann
parents:
diff changeset
    45
    if ($first == 1) {
e634d33deb86 added new website
haftmann
parents:
diff changeset
    46
      $first = 0;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    47
    }
e634d33deb86 added new website
haftmann
parents:
diff changeset
    48
    else {
e634d33deb86 added new website
haftmann
parents:
diff changeset
    49
      print OUT $listFooter;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    50
    }
e634d33deb86 added new website
haftmann
parents:
diff changeset
    51
    print OUT $topicStart;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    52
    print OUT $1;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    53
    print OUT $topicEnd;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    54
    print OUT $listHeader;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    55
  }
e634d33deb86 added new website
haftmann
parents:
diff changeset
    56
  elsif (/^[ \t]+([^ \t]+)[ \t]+(.+)\n/) {
e634d33deb86 added new website
haftmann
parents:
diff changeset
    57
    print OUT $lineHeader;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    58
    print OUT "<a target='_blank' href='$path$1.pdf'>$2</a>";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    59
    print OUT $lineEnd;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    60
  }
e634d33deb86 added new website
haftmann
parents:
diff changeset
    61
}
e634d33deb86 added new website
haftmann
parents:
diff changeset
    62
e634d33deb86 added new website
haftmann
parents:
diff changeset
    63
print OUT $listFooter;
e634d33deb86 added new website
haftmann
parents:
diff changeset
    64
e634d33deb86 added new website
haftmann
parents:
diff changeset
    65
print OUT '</dummy:wrapper>' . "\n";
e634d33deb86 added new website
haftmann
parents:
diff changeset
    66
e634d33deb86 added new website
haftmann
parents:
diff changeset
    67
close(OUT);
e634d33deb86 added new website
haftmann
parents:
diff changeset
    68
close(IN);
e634d33deb86 added new website
haftmann
parents:
diff changeset
    69
e634d33deb86 added new website
haftmann
parents:
diff changeset
    70
exit(0);