]> matita.cs.unibo.it Git - helm.git/commitdiff
Another patch to the http_getter.ml.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 16 Nov 2000 15:44:12 +0000 (15:44 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 16 Nov 2000 15:44:12 +0000 (15:44 +0000)
Now with getwithtypes it retrieves also annotations.

helm/interface/http_getter/http_getter.pl

index d534e90b262b87b1ce5926eff20aeca66597f71a..1d99e65ce03bf5b552adf1c8e1a5451b07f03172 100755 (executable)
@@ -148,19 +148,38 @@ EOT
             $res->content($merged);
             $c->send_response($res);
         } elsif ($http_method eq 'GET' and $http_path eq "/getwithtypes") {
-            my $do_annotate = ($cicuri =~ /\.types$/);
+            my $mode;
+            my $do_annotate;
+            if ($cicuri =~ /\.types$/) {
+               $do_annotate = 1;
+               $mode = "types";
+            } elsif ($cicuri =~ /\.ann$/) {
+               $do_annotate = 1;
+               $mode = "ann";
+            } else {
+               $do_annotate = 0;
+            }
             my $target_to_annotate = $cicuri;
-            $target_to_annotate =~ s/(.*)\.types$/$1/ if $do_annotate;
+            if ($mode eq "types") {
+               $target_to_annotate =~ s/(.*)\.types$/$1/;
+            } elsif ($mode eq "ann") {
+               $target_to_annotate =~ s/(.*)\.ann$/$1/;
+            }
             my $filename = $cicuri;
             $filename =~ s/cic:(.*)/$1/;
             $filename =~ s/theory:(.*)/$1/;
             my $filename_target = $helm_dir.$filename if $do_annotate;
             $filename = $helm_dir.$filename.".xml";
-            $filename_target =~ s/(.*)\.types$/$1.xml/ if $do_annotate;
+            if ($mode eq "types") {
+               $filename_target =~ s/(.*)\.types$/$1.xml/;
+            } elsif ($mode eq "ann") {
+               $filename_target =~ s/(.*)\.ann$/$1.xml/;
+            }
             my $resolved = $map{$cicuri};
             my $resolved_target = $map{$target_to_annotate} if $do_annotate;
             if ($do_annotate) {
-               print "GETWITHTYPES!!\n";
+               print "GETWITHTYPES!!\n" if ($mode eq "types");
+               print "GETWITHANN!!\n" if ($mode eq "ann");
                print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n";
              } else {
                print "$cicuri ==> $resolved ($filename)\n";
@@ -169,17 +188,20 @@ EOT
             # Retrieves the annotation
 
             if (stat($filename)) {
-               print "Using local copy for the types\n";
+               print "Using local copy for the types\n" if ($mode eq "types");
+               print "Using local copy for the ann\n" if ($mode eq "ann");
                open(FD, $filename);
                while(<FD>) { $cont .= $_; }
                close(FD);
             } else {
-               print "Downloading the types\n";
+               print "Downloading the types\n" if ($mode eq "types");
+               print "Downloading the ann\n" if ($mode eq "ann");
                $ua = LWP::UserAgent->new;
                $request = HTTP::Request->new(GET => "$resolved");
                $response = $ua->request($request, \&callback);
                
-               print "Storing file for the types\n";
+               print "Storing file for the types\n" if ($mode eq "types");
+               print "Storing file for the ann\n" if ($mode eq "ann");
                mkdirs($filename);
                open(FD, ">".$filename);
                print FD $cont;
@@ -221,13 +243,21 @@ EOT
             $target =~ s/<!DOCTYPE [^>]*>//sg;
             $annotation =~ s/<\?xml [^?]*\?>//sg;
             $annotation =~ s/<!DOCTYPE [^>]*>//sg;
+            my $element, $endelement; 
+            if ($mode eq "types") {
+               $element = "<ALLTYPES>";
+               $endelement = "</ALLTYPES>";
+            } elsif ($mode eq "ann") {
+               $element = "";
+               $endelement = "";
+            }
             my $merged = <<EOT;
 <?xml version="1.0" encoding="UTF-8"?>
 <cicxml uri="$target_to_annotate">
 $target
-<ALLTYPES>
+$element
 $annotation
-</ALLTYPES>
+$endelement
 </cicxml>
 EOT