From: Stefano Zacchiroli Date: Mon, 12 Feb 2001 21:28:23 +0000 (+0000) Subject: modified "update" request handling, now getter rebuild urls_of_uris.db. X-Git-Tag: v0_1_2~120 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fe24653b699d2fdb49834653dd8480438c9dc545;p=helm.git modified "update" request handling, now getter rebuild urls_of_uris.db. (feature moved from mmlinterface to http_getter) Also modified file 'getter.ml' from module 'interface' --- diff --git a/helm/http_getter/http_getter.pl.in b/helm/http_getter/http_getter.pl.in index 89f496ac7..5710c40ff 100755 --- a/helm/http_getter/http_getter.pl.in +++ b/helm/http_getter/http_getter.pl.in @@ -290,9 +290,9 @@ EOT $cont = "$quoted_html_link"; answer($c,$cont); } elsif ($http_method eq 'GET' and $http_path eq "/update") { - print "Update requested..."; - update(); - kill(USR1,getppid()); + print "Update requested...\n"; + mk_urls_of_uris(); + kill(USR1,getppid()); # signal changes to parent print " done\n"; answer($c,"

Update done

"); } elsif ($http_method eq 'GET' and $http_path eq "/version") { @@ -464,7 +464,75 @@ sub answer $c->send_response($res); } +sub helm_wget { +#ported from helm_wget executable, TODO: rewrite without wget. +#retrieve a file from an url and write it to a temp dir +#used for retrieve resource indexe from servers + my ($prefix, $URL) = @_; + if ($URL =~ /^file:\//) { + $URL =~ s/^file:\///; + my $command = "mkdir -p $prefix ; cp $URL $prefix"; + print "$command\n"; + system($command) == 0 + or die "\"$command\" error"; + } else { + my $command = "wget -c -P $prefix $URL"; + system($command) == 0 + or die "\"$command\" error"; + } +} + sub update { untie %map; tie(%map, 'DB_File', $uris_dbm.".db", O_RDONLY, 0664); } + +sub mk_urls_of_uris { +#rebuild $uris_dbm.db fetching resource indexes from servers + my ( + $server, $idxfile, $uri, $url, $comp, $line, + @servers, + %urls_of_uris + ); + + untie %map; + if (stat $uris_dbm.".db") { # remove old db file + unlink($uris_dbm.".db") or + die "cannot unlink old db file: $uris_dbm.db\n"; + } + tie(%urls_of_uris, 'DB_File', $uris_dbm.".db", O_RDWR|O_CREAT, 0664); + + open (SRVS, "< $servers_file") or + die "cannot open servers file: $servers_file\n"; + @servers = ; + close (SRVS); + while ($server = pop @servers) { #cicle on servers in reverse order + print "processing server: $server ...\n"; + chomp $server; + $debugserver = "http://dalamar.krynn.it/helm"; # FOR DEBUG ONLY: REMOVE ME !! + helm_wget($tmpdir, $debugserver."/".$indexname); #get index + $idxfile = $tmpdir."/".$indexname; + open (INDEX, "< $idxfile") or + die "cannot open temporary index file: $idxfile\n"; + while ($line = ) { #parse index and add entry to urls_of_uris + chomp $line; + ($uri,$comp) = split /[ \t]+/, $line; + # build url: + if ($comp =~ /gz/) { + $url = $uri . ".xml" . ".gz"; + } else { + $url = $uri . ".xml"; + } + $url =~ s/cic:/$server/; + $url =~ s/theory:/$server/; + $urls_of_uris{$uri} = $url; + } + close INDEX; + die "cannot unlink temporary file: $idxfile\n" + if (unlink $idxfile) != 1; + } + + untie(%urls_of_uris); + tie(%map, 'DB_File', $uris_dbm.".db", O_RDONLY, 0664); +} +