X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fgraphs%2Ftools%2Furi_set_queue.cgi;h=6a5d16ad51949042a9faaa82984004b0400549ef;hb=c5c48f3d3515f1dd95657245922ec1f340e17f70;hp=4c66515288a269f352bde72483c4cc25eb2e81aa;hpb=e85bc43c20254aa85463748eeb95e2e60ed0ccf1;p=helm.git

diff --git a/helm/graphs/tools/uri_set_queue.cgi b/helm/graphs/tools/uri_set_queue.cgi
index 4c6651528..6a5d16ad5 100755
--- a/helm/graphs/tools/uri_set_queue.cgi
+++ b/helm/graphs/tools/uri_set_queue.cgi
@@ -5,21 +5,25 @@ use HTTP::Status;
 use HTTP::Response;
 use CGI;
 
-my $d = new HTTP::Daemon LocalPort => 8084;
+$urisetqueueport = $ENV{'URI_SET_QUEUE_PORT'} || $urisetqueueport;
+
+my $d = new HTTP::Daemon LocalPort => $urisetqueueport
+ or die "Error: port $urisetqueueport not available.";
 print "Please contact me at: <URL:", $d->url, ">\n";
 
 $SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes
 
 my %uri_sets;
 my %uri_queues;
+my %overflowed;
+my %size;
 
-#NOT REENTRANT: CAN NOT FORK DUE TO THE GLOBAL VARIABLES %uri_sets & %uri_queues
+#NOT REENTRANT: CAN NOT FORK DUE TO THE GLOBAL VARIABLES %uri_sets & ...
 #HENCE, THE "PID" ARGUMENT OF EVERY REQUEST MUST IDENTIFY THE SET OF URI
 #IT WANTS TO WORK WITH. MOREOVER, EVERY CLIENT MUST WORK WITH A DIFFERENT SET
 #OF URI, I.E. EVERY PID MUST BE UNIQUE.
 
 #CSC: WHAT IF THE CLIENTS ARE ON DIFFERENT MACHINES AND HAVE THE SAME PID?
-#CSC: CGI MODULE REQUIRED TO PROCESS PARAMETERS BETTER
 
 while (my $c = $d->accept) {
     while (my $r = $c->get_request) {
@@ -32,14 +36,14 @@ while (my $c = $d->accept) {
             print(@{$uri_queues{$pid}} + 0);
             print "/";
             my $tot = keys(%{$uri_sets{$pid}}) + 0;
+            $tot .= "*" if defined($overflowed{$pid});
 	    print "$tot $uri: ";
 
             my $res;
 	    if (!(defined($uri_sets{$pid}->{$uri}))) {
-                if ($tot + 1 > 20) {
-	           $uri_sets{$pid}->{$uri} = -1;
-                   push @{$uri_queues{$pid}},$uri;
-                   $res = "added_with_mark";
+                if ($tot + 1 > $size{$pid}) {
+                   $res = "not_added_because_already_too_many";
+                   $overflowed{$pid} = 1;
                 } else {
 	           $uri_sets{$pid}->{$uri} = 1;
                    push @{$uri_queues{$pid}},$uri;
@@ -54,6 +58,32 @@ while (my $c = $d->accept) {
             $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
 	    $response->content_type('text/xml');
             $c->send_response($response);
+        } elsif ($r->method eq 'GET' and $r->url->path eq '/is_overflowed') {
+            my $http_query = $r->url->equery;
+            my $cgi = new CGI("$http_query");
+            my $pid = $cgi->param('PID');
+	    print "$pid: ";
+            print(@{$uri_queues{$pid}} + 0);
+            print "/";
+	    print(keys(%{$uri_sets{$pid}}) + 0);
+            print "*" if defined($overflowed{$pid});
+            my $res = defined($overflowed{$pid}) ? "true" : "false";
+            print " is_overflowed: $res\n";
+	    my $response = new HTTP::Response;
+            $response->content("<?xml version=\"1.0\"?>\n<$res/>\n");
+	    $response->content_type('text/xml');
+            $c->send_response($response);
+        } elsif ($r->method eq 'GET' and $r->url->path eq '/set_uri_set_size') {
+            my $http_query = $r->url->equery;
+            my $cgi = new CGI("$http_query");
+            my $pid = $cgi->param('PID');
+            my $size = $cgi->param('size');
+	    print "$pid: size := $size\n";
+            $size{$pid} = $size;
+	    my $response = new HTTP::Response;
+            $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
+	    $response->content_type('text/xml');
+            $c->send_response($response);
         } elsif ($r->method eq 'GET' and $r->url->path eq '/get_next') {
             my $http_query = $r->url->equery;
             my $cgi = new CGI("$http_query");
@@ -62,22 +92,23 @@ while (my $c = $d->accept) {
             print(@{$uri_queues{$pid}} + 0);
             print "/";
 	    print(keys(%{$uri_sets{$pid}}) + 0);
+            print "*" if defined($overflowed{$pid});
             print " ";
 
             my $elem = shift @{$uri_queues{$pid}};
-            my $mark = $uri_sets{$pid}->{$elem};
+            my $mark = $overflowed{$pid};
 
 	    my $response = new HTTP::Response;
             my $xml_header = "<?xml version=\"1.0\"?>\n";
-            if ($mark == 1) {
-	       print "$elem removed\n";
-               $response->content("$xml_header<uri value=\"$elem\"/>\n");
-            } elsif ($mark == -1) {
+            if (!defined($elem)) {
+	       print "is now empty\n";
+               $response->content("$xml_header<empty/>\n");
+            } elsif ($mark == 1) {
 	       print "$elem (marked) removed\n";
                $response->content("$xml_header<marked_uri value=\"$elem\"/>\n");
             } else {
-	       print "is now empty\n";
-               $response->content("$xml_header<empty/>\n");
+	       print "$elem removed\n";
+               $response->content("$xml_header<uri value=\"$elem\"/>\n");
             }
 	    $response->content_type('text/xml');
             $c->send_response($response);
@@ -92,10 +123,17 @@ while (my $c = $d->accept) {
             }
 	    print "************\nThe URI set $pid is now empty again\n";
 	    delete($uri_sets{$pid});
+            delete($overflowed{$pid});
+            delete($size{$pid});
 	    my $response = new HTTP::Response;
             $response->content("<?xml version=\"1.0\"?>\n<done/>\n");
 	    $response->content_type('text/xml');
             $c->send_response($response);
+        } elsif ($r->method eq 'GET' && $r->url->path eq "/help"){
+           print "Help requested!\n";
+	   my $response = new HTTP::Response;
+           $response->content("URI-Set (Queue) Version: ???");
+           $c->send_response($response);
         } else {
             $c->send_error(RC_FORBIDDEN)
         }