]> matita.cs.unibo.it Git - helm.git/blob - helm/cgi/mkindextheory.pl
New on-line interface
[helm.git] / helm / cgi / mkindextheory.pl
1 #!/usr/bin/perl
2
3 # First of all, let's load HELM configuration
4 use Env;
5 my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"};
6 # this should be the only fixed constant
7 my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm";
8 if (defined ($HELM_LIB_DIR)) {
9    $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl";
10 } else {
11    $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl";
12 }
13
14 # next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm
15 require $HELM_LIB_PATH;
16
17 use URI::Escape;
18 use LWP::UserAgent;
19 use CGI;
20
21 my $cgi = new CGI($ENV{"REQUEST_URL"});
22 $uri = $cgi->param('theoryuri');
23 $uri =~ s/(.*)\/$/$1/; # Remove a final slash if present
24 $uri .= "/"; # Put a final slash
25 $myurl = $cgi->url();
26
27 $cont = ""; # modified by side-effect by &callback
28 my $ua = LWP::UserAgent->new;
29 my $request = HTTP::Request->new(GET => $getter_url."ls?format=txt&baseuri=".$uri);
30 my $response = $ua->request($request, \&callback);
31  
32 @filenames = split(/\n/, $cont);
33
34 my $uridotdot = $uri;
35 $uridotdot =~ s/(.*)\/.+/$1/;
36 if ($uri ne "theory:/") {
37  # Let's print the link to the parent directory
38  $output = <<EOT;
39 <tr>
40 <td><img border="0" src="/icons/back.gif" alt="[BACK]"></td>
41 <td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddentheoryuri.value='$uridotdot'; refreshReload(); refreshTheoryHeader(); this.search='?theoryuri=$uridotdot';" onMouseOver="window.status='$uridotdot'; return true">Parent Directory</a></td>
42 </tr>
43 EOT
44 }
45
46 foreach $i (@filenames) {
47    my ($type,$name) = split(/,/, $i);
48    if ($type eq "dir") {
49       $output .= <<EOT;
50 <tr>
51 <td><img border="0" src="/icons/folder.gif" alt="[DIR]"></td>
52 <td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddentheoryuri.value='$uri$name'; refreshReload(); refreshTheoryHeader(); this.search='?theoryuri=$uri$name';" onMouseOver="window.status='$uri$name'; return true">$name</a></td>
53 </tr>
54 EOT
55    } elsif ($type eq "object") {
56          if ($name =~ /\.theory$/) {
57             # theory file
58             $output .= <<EOT;
59 <tr>
60 <td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
61 <td><a href="" target="theory" onClick="this.href=makeURL('theory','$uri$name','$processor_url','$getter_url')" onMouseOver="window.status='$uri$name'; return true">$name</a>
62 </tr>
63 EOT
64          } else {
65             $output .= <<EOT;
66 <tr>
67 <td><img border="0" src="/icons/unknown.gif" alt="[DIR]"></td>
68 <td>$name</td>
69 </tr>
70 EOT
71          }
72    } else {
73       $output .= <<EOT;
74 <tr>
75 <td><img border="0" src="/icons/burst.gif" alt="[DIR]"></td>
76 <td>$name</td>
77 </tr>
78 EOT
79    }
80 }
81
82 print <<EOT;
83 Content-type: text/html
84
85 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
86 "http://www.w3.org/TR/REC-html40/loose.dtd">
87 <html>
88 <head>
89 <title>Index of $uri</title>
90 <script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
91 </script>
92 </head>
93 <body bgcolor="#ffffff" text="#000000">
94 <table>
95 $output
96 </table>
97 <hr noshade align="left" width="80%">
98 </body>
99 </html>
100 EOT
101
102 #================================
103
104 sub callback
105 {
106  my ($data) = @_;
107  $cont .= $data;
108 }