Admin/page/bin/mkcontents
author haftmann
Mon, 06 Jun 2005 14:12:07 +0200
changeset 16301 f9f2e1643593
parent 14490 7b37aa726d2d
permissions -rwxr-xr-x
migrated scripts to new webiste
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
14490
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    27
$listHeader = "<ul>\n";
12732
wenzelm
parents: 9699
diff changeset
    28
$lineHeader = "  <li>";
wenzelm
parents: 9699
diff changeset
    29
$lineEnd    = "</li>\n";
14490
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    30
$listFooter = "</ul>\n";
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    31
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    32
$topicStart = "<h2>";
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    33
$topicEnd   = "</h2>\n";
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    34
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
open(IN, "<$infile") || die "cannot read input file <$infile>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    36
open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
14490
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    38
$first = 1;
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    39
while (<IN>) {
14490
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    40
  if (/^([^ \t].*)\n/) {
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    41
    if ($first == 1) {
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    42
      $first = 0;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    43
    }
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    44
    else {
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    45
      print OUT $listFooter;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    46
    }
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    47
    print OUT $topicStart;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    48
    print OUT $1;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    49
    print OUT $topicEnd;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    50
    print OUT $listHeader;
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    51
  }
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    52
  elsif (/^[ \t]+([^ \t]+)[ \t]+(.+)\n/) {
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    53
    print OUT $lineHeader;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    54
    print OUT "<a href=\"$path$1.pdf\">$2</a>";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    55
    print OUT $lineEnd;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    56
  }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    57
}
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    58
14490
7b37aa726d2d allow sections in contents file
kleing
parents: 12732
diff changeset
    59
print OUT $listFooter;
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    60
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    61
close(OUT);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    62
close(IN);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    63
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    64
exit(0);