]> matita.cs.unibo.it Git - helm.git/commitdiff
Added preliminary support for gzipped library
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 15 Jan 2001 12:58:05 +0000 (12:58 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 15 Jan 2001 12:58:05 +0000 (12:58 +0000)
helm/http_getter/AUTHORS
helm/http_getter/http_getter.pl.in

index 1088c56891151e79d009722f2b7533c28ca3040d..72c65aaa008e0d1ddd0654b63dfbd584e33452eb 100644 (file)
@@ -1 +1,2 @@
 Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>
+Stefano Zacchiroli <zacchiro@cs.unibo.it>
index e8adb3bc02f321d0c3ca1adc05b4f894749c0758..9c68ae71077c7e97ee7ffc87ffd719fd19cab60c 100755 (executable)
@@ -41,6 +41,7 @@ use HTTP::Status;
 use HTTP::Request;
 use LWP::UserAgent;
 use DB_File;
+use Compress::Zlib;
 
 #CSC: mancano i controlli sulle condizioni di errore di molte funzioni
 #CSC: ==> non e' robusto
@@ -72,9 +73,21 @@ while (my $c = $d->accept) {
             my $cicfilename = $cicuri;
             $cicfilename =~ s/cic:(.*)/$1/;
             $cicfilename =~ s/theory:(.*)/$1/;
-            $cicfilename = $helm_dir.$cicfilename.".xml";
-
+#            $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'";
+                       }
+            $cicfilename = $helm_dir.$cicfilename.$extension;
+
+            #my $cicurl   = $map{$cicuri};
+# </gzip>
             if (!defined($cicurl)) {
              print "\nNOT FOUND!!!!!\n";
              $c->send_error(RC_NOT_FOUND)
@@ -114,13 +127,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";
+#            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 $typesuri;
-            my $annurl   = $map{$annuri}  if $annuri;
+            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 $typesfilename = $cicfilename.$typesext if $typesuri;
+            my $annfilename  = $cicfilename.$annsuffix.$annext if $annuri;
+            $cicfilename .= $cicext;
+# </gzip>
+
 
             if (!defined($cicurl) ||
                (!defined($typesurl) && $typesuri) ||
@@ -234,14 +279,40 @@ sub callback
 sub download
 {
  my ($remove_headers,$str,$url,$filename) = @_;
+# <gzip>
+ my ($gz, $buffer);
+
+ my $mode;     # retrieve mode: "normal" (.xml) or "gzipped" (.xml.gz)
+ if ($filename =~ /\.xml$/) {  # set retrieve mode
+        $mode = "normal";
+ } elsif ($filename =~ /\.xml\.gz$/) {
+        $mode = "gzipped";
+ } else {
+        die "Unsupported download extension, might be '.gz' or '.xml'\n";
+ }
+# </gzip>
  $cont = ""; # modified by side-effect by the callback function
- if (stat($filename)) {
+ if (stat($filename)) {                # we already have local copy of requested file
     print "Using local copy for the $str file\n";
-    open(FD, $filename);
-    while(<FD>) { $cont .= $_; }
-    close(FD);
- } else {
-    print "Downloading the $str file\n";
+# <gzip>
+       if ($mode eq "gzipped") {       # deflating cached file
+               print "deflating local file ...\n";
+               $gz = gzopen($filename, "r") or die "Cannot open gzip'ed file $filename: $gzerrno";
+               while ( $gz->gzread($buffer) > 0 ) {
+                       $cont .= $buffer;
+               }
+               die "Error while reading : $gzerrno\n" if $gzerrno != Z_STREAM_END ;
+               $gz->gzclose();
+       } elsif ($mode eq "normal") {   # return cached file
+               open(FD, $filename);
+               while(<FD>) { $cont .= $_; }
+               close(FD);
+       } else {        # error
+               die "Internal error: unexpected mode: $mode, might be 'normal' or 'gzipped'";
+       }
+# </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);
@@ -251,6 +322,19 @@ sub download
     open(FD, ">".$filename);
     print FD $cont;
     close(FD);
+# <gzip>
+       if ($mode eq "gzipped") {       # deflate gzipped retrieved file
+               print "deflating just retrieved file ...\n";
+               $cont = "";             # reset $cont, cause $cont actually contain gzipped data
+               $gz = gzopen($filename, "r") or die "Cannot open gzip'ed file $filename: $gzerrno";
+               while ( $gz->gzread($buffer) > 0 ) {
+                       $cont .= $buffer;
+               }
+               die "Error while reading : $gzerrno\n" if $gzerrno != Z_STREAM_END ;
+               $gz->gzclose();
+                       # now $cont contain deflated, clear text data
+       }
+# </gzip>
  }
  if ($remove_headers) {
     $cont =~ s/<\?xml [^?]*\?>//sg;