Admin/page/common/functions.pl
author wenzelm
Thu, 15 Nov 2001 18:20:13 +0100
changeset 12207 4dff931b852f
parent 10344 bb0b65380516
child 15427 4b939ba65c31
permissions -rw-r--r--
added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     1
<!-- _GP_
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     2
# undef all the functions we're defining. This stops lots of
9920
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
     3
# complaining about re-defining the sub for each content file that's
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     4
# processed.
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     5
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
     6
       if (defined(&me)) { undef &me; }
9920
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
     7
       if (defined(&distname)) { undef &distname; }
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
     8
       if (defined(&href)) { undef &href; }
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
     9
       if (defined(&twodig)) { undef &twodig; }
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    10
       if (defined(&when)) { undef &when; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    11
       if (defined(&size)) { undef &size; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    12
       if (defined(&page)) { undef &page; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    13
       if (defined(&empty_line)) { undef &empty_line; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    14
       if (defined(&setnavcolor)) { undef &setnavcolor; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    15
       if (defined(&twodig)) { undef &twodig; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    16
       if (defined(&setdowncolor)) { undef &setdowncolor; }
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
    17
       if (defined(&downloadhead)) { undef &downloadhead; }
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    18
       if (defined(&download)) { undef &download; }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    19
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    20
 -->
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    21
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    22
<!--  _GP_ 
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    23
9920
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    24
    sub distname {
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    25
      return $ENV{"DISTNAME"};
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    26
    }
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    27
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    28
    sub href {
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    29
	return "<a href=\"" . $_[0] . "\">" . $_[1] . "</a>";
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    30
    }
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
    31
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    32
    sub twodig {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    33
      if ($_[0] < 10) {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    34
        return "0$_[0]";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    35
      }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    36
      return "$_[0]";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    37
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    38
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    39
# ($sec,$min,$hour,$mday,$mon,$year,$wday,$yday,$isdst) = gmtime(time);     
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    40
    sub when { 
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    41
      my @s = stat $inputfile;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    42
      my @t = gmtime($s[9]);      
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    43
      my $year  = $t[5]+1900;      
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    44
      my $month = twodig($t[4]+1);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    45
      my $day   = twodig($t[3]);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    46
      return "$month/$day/$year";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    47
#      my $hour  = twodig($t[2]);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    48
#      my $min   = twodig($t[1]);
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    49
#      return "$month/$day/$year $hour:$min UTC";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    50
    }  
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    51
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    52
    sub setnavcolor {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    53
      $navcolor = $_[0];
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    54
      return "";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    55
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    56
    
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    57
    # page(name, file)
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    58
    sub page {    
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    59
      my $retval = "";      
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    60
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    61
      if ("$_[1].html" eq substr($outputfile,rindex($outputfile,"/")+1)) {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    62
        $retval = <<EOF;
10344
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    63
        <table width="188" border="0" cellspacing="0" cellpadding="5">
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    64
        <tr> 
10344
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    65
          <td width="8" bgcolor="$navcolor">&nbsp;</td>
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    66
          <td width="160" align="center" bgcolor="$navcolor">
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    67
            <b><font face="Arial,Helvetica"><A HREF="$_[1].html" target="_top">$_[0]</A></font></b>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    68
          </td>
10344
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    69
          <td width="8" bgcolor="$navcolor">&nbsp;</td>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    70
        </tr>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    71
        </table>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    72
EOF
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    73
      }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    74
      else {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    75
        $retval = <<EOF;
10344
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    76
        <table width="188" border="0" cellspacing="0" cellpadding="5">
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    77
        <tr> 
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    78
          <td width="8">&nbsp;</td>
10344
bb0b65380516 cleanup, looks ok now with konqueror, too
kleing
parents: 10085
diff changeset
    79
          <td width="160" align=center bgcolor="$navcolor">
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    80
            <b><font face="Arial,Helvetica"><A HREF="$_[1].html" target="_top">$_[0]</A></font></b>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    81
          </td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    82
          <td width="8">&nbsp;</td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    83
        </tr>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    84
        </table>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    85
EOF
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    86
      }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    87
      return $retval;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    88
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    89
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    90
    # empty_line(numcols)
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    91
    sub empty_line {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    92
      my $retval = <<EOF;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    93
      <p>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    94
EOF
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    95
      return $retval;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    96
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    97
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    98
    sub size {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
    99
      my $filename = $_[0];
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   100
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   101
      my @s = stat $filename;
9920
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
   102
      my $size = defined $s[7] ? $s[7]/1024 : 0;
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   103
9925
wenzelm
parents: 9920
diff changeset
   104
      return sprintf("%d", $size);
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   105
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   106
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   107
    sub setdowncolor {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   108
      $downcolor = $_[0];
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   109
      return "";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   110
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   111
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   112
    sub downloadhead {
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   113
      my $text = $_[0];
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   114
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   115
      return <<EOF;
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   116
      <tr><td colspan=3><strong>$text</strong></td></tr>
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   117
EOF
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   118
    }
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   119
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   120
    sub download {
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   121
      my $rowspan = $_[0];
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   122
      my $descr = $_[1];
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   123
      my $url   = $_[2];
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   124
      my $prefix  = $_[3];
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   125
9920
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
   126
      my $size = size("$prefix/$url");
9734f2717203 improved WWW page generation (still somewhat experimental);
wenzelm
parents: 8056
diff changeset
   127
      $size = "$size K";
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   128
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   129
      my $filename = $path;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   130
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   131
      if ($url =~ /([^\/]*\/)*([^\/]+)/) {
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   132
	$filename = $2;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   133
      }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   134
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   135
      my $td   = "nowrap bgcolor=$downcolor";
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   136
      
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   137
      my $descr_text = "";
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   138
      if ($descr ne "") {
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   139
        $descr_text = <<EOF;
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   140
	<td rowspan=$rowspan align="left" $td>
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   141
          &nbsp; $descr
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   142
        </td>
10085
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   143
EOF
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   144
      }
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   145
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   146
      my $retval = <<EOF;
a9704bf90031 simplified;
wenzelm
parents: 9925
diff changeset
   147
      <tr>$descr_text
8056
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   148
        <td align="left" $td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   149
          &nbsp; <A HREF="$url">$filename</A>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   150
        </td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   151
        <td align="right" $td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   152
          &nbsp; $size &nbsp;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   153
        </td>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   154
      </tr>
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   155
EOF
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   156
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   157
      return $retval;
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   158
    }
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   159
3c587e7b8fe5 new webpage layout
kleing
parents:
diff changeset
   160
 -->