]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/http_getter/http_getter.pl.in
This commit was manufactured by cvs2svn to create tag 'v0_0_2'.
[helm.git] / helm / http_getter / http_getter.pl.in
index b1ec80aeb972c3a0dc7941f8da67a2b0574deb68..43c7ff0790ec3750ce8858c6a54e972071a269c9 100755 (executable)
@@ -34,16 +34,11 @@ if (defined ($HELM_LIB_DIR)) {
    $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl";
 }
 
-# Let's override the configuration file
-$styles_dir = $ENV{"HELM_STYLE_DIR"} if (defined ($ENV{"HELM_STYLE_DIR"}));
-$dtd_dir = $ENV{"HELM_DTD_DIR"} if (defined ($ENV{"HELM_DTD_DIR"}));
-
 # <ZACK>: TODO temporary, move this setting to configuration file
 # set the cache mode, may be "gzipped" or "normal"
 my $cachemode = $ENV{'HTTP_GETTER_CACHE_MODE'} || 'gzipped';
 if (($cachemode ne 'gzipped') and ($cachemode ne 'normal')) {
- die "Invalid HTTP_GETTER_CACHE_MODE environment variable, must be".
- "'normal' or 'gzipped'\n";
+       die "Invalid HTTP_GETTER_CACHE_MODE environment variable, must be 'normal' or 'gzipped'\n";
 }
 # </ZACK>
 
@@ -89,19 +84,21 @@ while (my $c = $d->accept) {
             my $cicfilename = $cicuri;
             $cicfilename =~ s/cic:(.*)/$1/;
             $cicfilename =~ s/theory:(.*)/$1/;
-
+#            $cicfilename = $helm_dir.$cicfilename.".xml";
+# <gzip>
             my $cicurl   = $map{$cicuri};
-            my $extension;
-            if ($cicurl =~ /\.xml$/) { # non gzipped file
-              $extension = ".xml";
-            } elsif ($cicurl =~ /\.xml\.gz$/) { # gzipped file
-              $extension = ".xml.gz";
-            } else { # error: unknown extension
-             die "unexpected extension in url: $cicurl, might be '.xml'".
-              "or '.xml.gz'";
-            }
+                       my $extension;
+                       if ($cicurl =~ /\.xml$/) {      # non gzipped file
+                                       $extension = ".xml";
+                       } elsif ($cicurl =~ /\.xml\.gz$/) {     # gzipped file
+                                       $extension = ".xml.gz";
+                       } else {        # error: unknown extension
+                               die "unexpected extension in url: $cicurl, might be '.xml' or '.xml.gz'";
+                       }
             $cicfilename = $helm_dir.$cicfilename.$extension;
 
+            #my $cicurl   = $map{$cicuri};
+# </gzip>
             if (!defined($cicurl)) {
              print "\nNOT FOUND!!!!!\n";
              $c->send_error(RC_NOT_FOUND)
@@ -141,41 +138,45 @@ while (my $c = $d->accept) {
             $cicfilename =~ s/theory:(.*)/$1/;
             $cicfilename = $helm_dir.$cicfilename;
 
+#            my $typesfilename = $cicfilename.".types.xml"     if $typesuri;
+#            my $annfilename  = $cicfilename.$annsuffix.".xml" if $annuri;
+#            $cicfilename .= ".xml";
+
+# <gzip>
             my $cicurl   = $map{$cicuri};
             my $typesurl = $map{$typesuri} if (defined($typesuri));
             my $annurl   = $map{$annuri}  if (defined($annuri));
-            my ($cicext, $typesext, $annext);
-            if ($cicurl =~ /\.xml$/) { # normal file
-             $cicext = ".xml";
-            } elsif ($cicurl =~ /\.xml\.gz$/) { # gzipped file
-             $cicext = ".xml.gz";
-            } else {
-             die "unexpected extension in url: $cicurl;".
-             "might be '.xml' or '.xml.gz'";
-            }
-            if (defined($typesuri)) { # extension selection for types file
-             if ($typesurl =~ /\.xml$/) { # normal file
-              $typesext = ".types.xml";
-             } elsif ($typesurl =~ /\.xml\.gz$/) { # gzipped file
-              $typesext = ".types.xml.gz";
-             } else {
-              die "unexpected extension in url: $typesurl;".
-              "might be '.xml' or '.xml.gz'";
-             }
-            }
-            if (defined($annuri)) { # extension selection for annotation file
-             if ($annurl =~ /\.xml$/) { # normal file
-              $annext = ".xml";
-             } elsif ($annurl =~ /\.xml\.gz$/) { # gzipped file
-              $annext = ".xml.gz";
-             } else {
-              die "unexpected extension in url: $annurl".
-              "might be '.xml' or '.xml.gz'";
-             }
-            }
+                       my ($cicext, $typesext, $annext);
+                       if ($cicurl =~ /\.xml$/) {      # normal file
+                               $cicext = ".xml";
+                       } elsif ($cicurl =~ /\.xml\.gz$/) {     # gzipped file
+                               $cicext = ".xml.gz";
+                       } else {
+                               die "unexpected extension in url: $cicurl; might be '.xml' or '.xml.gz'";
+                       }
+                       if (defined($typesuri)) {       # extension selection for types file
+                               if ($typesurl =~ /\.xml$/) {    # normal file
+                                       $typesext = ".types.xml";
+                               } elsif ($typesurl =~ /\.xml\.gz$/) {   # gzipped file
+                                       $typesext = ".types.xml.gz";
+                               } else {
+                                       die "unexpected extension in url: $typesurl; might be '.xml' or '.xml.gz'";
+                               }
+                       }
+                       if (defined($annuri)) { # extension selection for annotation file
+                               if ($annurl =~ /\.xml$/) {      # normal file
+                                       $annext = ".xml";
+                               } elsif ($annurl =~ /\.xml\.gz$/) {     # gzipped file
+                                       $annext = ".xml.gz";
+                               } else {
+                                       die "unexpected extension in url: $annurl might be '.xml' or '.xml.gz'";
+                               }
+                       }
             my $typesfilename = $cicfilename.$typesext if $typesuri;
             my $annfilename  = $cicfilename.$annsuffix.$annext if $annuri;
             $cicfilename .= $cicext;
+# </gzip>
+
 
             if (!defined($cicurl) ||
                (!defined($typesurl) && $typesuri) ||
@@ -226,20 +227,6 @@ EOT
             } else {
                die "Could not find DTD!";
             }
-         } elsif ($http_method eq 'GET' and $http_path eq "/getxslt") {
-            my $filename = $inputuri;
-            $filename = $styles_dir."/".$filename;
-            print "XSLT: $inputuri ==> ($filename)\n";
-            if (stat($filename)) {
-               print "Using local copy\n";
-               open(FD, $filename) or die "Cannot open $filename\n";
-               $cont = "";
-               while(<FD>) { $cont .= $_; }
-               close(FD);
-               answer($c,$cont);
-            } else {
-               die "Could not find XSLT!";
-            }
         } elsif ($http_method eq 'GET' and $http_path eq "/conf") {
             my $quoted_html_link = $html_link;
             $quoted_html_link =~ s/&/&amp;/g;
@@ -306,8 +293,7 @@ sub gunzip { # gunzip a file and return the deflated content
        my ($gz, $buffer, $cont);
 
        print "deflating $filename ...\n";
-       $gz = gzopen($filename, "r")
-               or die "Cannot open gzip'ed file $filename: $gzerrno";
+       $gz = gzopen($filename, "r") or die "Cannot open gzip'ed file $filename: $gzerrno";
        $cont = "";
        while ( $gz->gzread($buffer) > 0 ) {
                $cont .= $buffer;
@@ -323,8 +309,7 @@ sub gzip {  # gzip the content argument and save it to filename argument
 
        my ($gz, $cont);
 
-       $gz = gzopen($filename, "w")
-               or die "Cannot gzopen for writing file $filename: $gzerrno";
+       $gz = gzopen($filename, "w") or die "Cannot gzopen for writing file $filename: $gzerrno";
        $gz->gzwrite($cont) or die "error writing: $gzerrno\n" ;
        $gz->gzclose();
 }
@@ -332,6 +317,7 @@ sub gzip {  # gzip the content argument and save it to filename argument
 sub download
 {
  my ($remove_headers,$str,$url,$filename) = @_;
+# <gzip>
  my ($gz, $buffer);
 
  my $resourcetype;     # retrieve mode: "normal" (.xml) or "gzipped" (.xml.gz)
@@ -343,7 +329,8 @@ sub download
         die "Unsupported download extension, might be '.gz' or '.xml'\n";
  }
  my $basefname = $filename;
- $basefname =~ s/\.gz$//;      # get base resource name removing trailing .gz
+ $basefname =~ s/\.gz$//;              # get base resource name removing trailing .gz
+# </gzip>
  $cont = ""; # modified by side-effect by the callback function
 
  my $localfname="";
@@ -352,60 +339,59 @@ sub download
  } elsif (stat($basefname.".gz")) {
        $localfname=$basefname.".gz";
  }
- if ($localfname ne "") { # we already have local copy of requested file
-      # check both possible cache entry: gzipped or normal
-  print "Using local copy for the $str file\n";
-  if ($localfname =~ /\.xml\.gz$/) { # deflating cached file and return it
-   $cont = gunzip($localfname);
-  } elsif ($localfname =~ /\.xml$/) { # just return cached file
-   open(FD, $localfname) or die "Cannot open $localfname";
-   while(<FD>) { $cont .= $_; }
-   close(FD);
-  } else { # error
-   die "Internal error: unexpected file name $localfname,"
-   ."must end with '.gz' or '.xml.gz'\n";
-  }
- } else { # download file from net
-    print "Downloading the $str file\n"; # download file
+ if ($localfname ne "") {              # we already have local copy of requested file
+                                                               # check both possible cache entry: gzipped or normal
+    print "Using local copy for the $str file\n";
+# <gzip>
+       if ($localfname =~ /\.xml\.gz$/) {      # deflating cached file and return it
+               $cont = gunzip($localfname);
+       } elsif ($localfname =~ /\.xml$/) {     # just return cached file
+               open(FD, $localfname) or die "Cannot open $localfname";
+               while(<FD>) { $cont .= $_; }
+               close(FD);
+       } else {        # error
+               die "Internal error: unexpected file name $localfname, must end with '.gz' or '.xml.gz'\n";
+       }
+# </gzip>
+ } else {      # download file from net
+    print "Downloading the $str file\n";       # download file
     $ua = LWP::UserAgent->new;
     $request = HTTP::Request->new(GET => "$url");
     $response = $ua->request($request, \&callback);
                
-    # cache retrieved file to disk
-# <ZACK/> TODO: inefficent, I haven't yet undestood how to deflate
-#    in memory gzipped file, without call "gzopen"
- print "Storing the $str file\n";
- mkdirs($filename);
- open(FD, ">".$filename.".tmp") or die "Cannot open $filename.tmp\n";
- print FD $cont;
- close(FD);
-
- # handle cache conversion normal->gzipped or gzipped->normal as user choice
- if (($cachemode eq 'normal') and ($resourcetype eq 'normal')) {
-   # cache the file as is
-  rename "$filename.tmp", $filename; 
- } elsif (($cachemode eq 'gzipped') and ($resourcetype eq 'gzipped')) {
-   # cache the file as is
-   # and update the $cont variabile with deflated content
-  rename "$filename.tmp", $filename; 
-  $cont = gunzip($filename);
- } elsif (($cachemode eq 'normal') and ($resourcetype eq 'gzipped')) {
-   # deflate cache entry
-   # and update $cont
-  open(FD, "> $basefname") or die "cannot open $basefname\n";
-  $cont = gunzip($filename.".tmp");
-  print FD $cont;
-  close(FD);
-  unlink "$filename.tmp"; # delete old gzipped file
- } elsif (($cachemode eq 'gzipped') and ($resourcetype eq 'normal')) {
-   # compress cache entry
-  gzip($cont, $basefname.".gz");
-  unlink "$filename.tmp"; # delete old uncompressed file
- } else {
-  die "Internal error, unsopported cachemode, resourcetype couple\n";
- }
- # $cont now contained uncompressed data
+                               # cache retrieved file to disk
+# <ZACK/> TODO: inefficent, I haven't yet undestood how to deflate in memory gzipped file,
+#                              without call "gzopen"
+# <gzip>
+       print "Storing the $str file\n";
+       mkdirs($filename);
+       open(FD, ">".$filename.".tmp") or die "Cannot open $filename.tmp\n";
+       print FD $cont;
+       close(FD);
+
+       # handle cache conversion normal->gzipped or gzipped->normal as user choice
+       if (($cachemode eq 'normal') and ($resourcetype eq 'normal')) { # cache the file as is
+               rename "$filename.tmp", $filename;      
+       } elsif (($cachemode eq 'gzipped') and ($resourcetype eq 'gzipped')) {  # cache the file as is
+                                                                                       # and update the $cont variabile with deflated content
+               rename "$filename.tmp", $filename;      
+               $cont = gunzip($filename);
+       } elsif (($cachemode eq 'normal') and ($resourcetype eq 'gzipped')) {   # deflate cache entry
+                                                                                                                                                       # and update $cont
+               open(FD, "> $basefname") or die "cannot open $basefname\n";
+               $cont = gunzip($filename.".tmp");
+               print FD $cont;
+               close(FD);
+               unlink "$filename.tmp"; # delete old gzipped file
+       } elsif (($cachemode eq 'gzipped') and ($resourcetype eq 'normal')) {   # compress cache entry
+               gzip($cont, $basefname.".gz");
+               unlink "$filename.tmp"; # delete old uncompressed file
+       } else {
+               die "Internal error, unsopported cachemode, resourcetype couple\n";
+       }
+       # $cont now contained uncompressed data
 
+# </gzip>
  }
  if ($remove_headers) {
     $cont =~ s/<\?xml [^?]*\?>//sg;