From: Stefano Zacchiroli Date: Sat, 3 Feb 2001 10:34:17 +0000 (+0000) Subject: Reindented some parts X-Git-Tag: v0_1_2~143 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=38034d883494780a817bb2d8cc30ac9b7d00b974;p=helm.git Reindented some parts --- diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in index addd81dcc..b1ec80aeb 100755 --- a/helm/http_getter/http_getter.pl.in +++ b/helm/http_getter/http_getter.pl.in @@ -42,7 +42,8 @@ $dtd_dir = $ENV{"HELM_DTD_DIR"} if (defined ($ENV{"HELM_DTD_DIR"})); # 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"; } # @@ -88,21 +89,19 @@ while (my $c = $d->accept) { my $cicfilename = $cicuri; $cicfilename =~ s/cic:(.*)/$1/; $cicfilename =~ s/theory:(.*)/$1/; -# $cicfilename = $helm_dir.$cicfilename.".xml"; -# + 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}; -# if (!defined($cicurl)) { print "\nNOT FOUND!!!!!\n"; $c->send_error(RC_NOT_FOUND) @@ -142,45 +141,41 @@ 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 $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; -# - if (!defined($cicurl) || (!defined($typesurl) && $typesuri) || @@ -311,7 +306,8 @@ 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; @@ -327,7 +323,8 @@ 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(); } @@ -335,7 +332,6 @@ sub gzip { # gzip the content argument and save it to filename argument sub download { my ($remove_headers,$str,$url,$filename) = @_; -# my ($gz, $buffer); my $resourcetype; # retrieve mode: "normal" (.xml) or "gzipped" (.xml.gz) @@ -347,8 +343,7 @@ 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 $cont = ""; # modified by side-effect by the callback function my $localfname=""; @@ -357,59 +352,60 @@ 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() { $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"; + 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() { $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 $ua = LWP::UserAgent->new; $request = HTTP::Request->new(GET => "$url"); $response = $ua->request($request, \&callback); - # cache retrieved file to disk -# 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 +# 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 -# } if ($remove_headers) { $cont =~ s/<\?xml [^?]*\?>//sg;