From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Nov 2000 10:15:16 +0000 (+0000)
Subject: Initial revision
X-Git-Tag: nogzip~171
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d66b34e7f8a6c6ceb330c4cfc8f6a3803eba262b;p=helm.git

Initial revision
---

diff --git a/helm/http_getter/cadet b/helm/http_getter/cadet
new file mode 100755
index 000000000..2b84119fa
--- /dev/null
+++ b/helm/http_getter/cadet
@@ -0,0 +1,9 @@
+#! /bin/sh
+
+# WARNING!!! No "//" in the middle of the path, nor a "/" at the end!!!!
+
+# For V6.2
+export HELM_CONFIGURATION_PREFIX=~/HELM/installation
+
+# For V7
+#export HELM_CONFIGURATION_PREFIX=/home/cadet/sacerdot
diff --git a/helm/http_getter/http_getter.pl b/helm/http_getter/http_getter.pl
new file mode 100755
index 000000000..1d99e65ce
--- /dev/null
+++ b/helm/http_getter/http_getter.pl
@@ -0,0 +1,329 @@
+#!/usr/bin/perl
+
+# First of all, let's load HELM configuration
+use Env;
+my $HELM_CONFIGURATION_PREFIX = $ENV{"HELM_CONFIGURATION_PREFIX"};
+my $HELM_CONFIGURATION_PATH =
+ $HELM_CONFIGURATION_PREFIX."/local/lib/helm/configuration.pl";
+# next require defines: $helm_dir, $html_link
+require $HELM_CONFIGURATION_PATH;
+
+
+
+use HTTP::Daemon;
+use HTTP::Status;
+use HTTP::Request;
+use LWP::UserAgent;
+use DB_File;
+
+my $cont = "";
+my $d = new HTTP::Daemon LocalPort => 8081;
+tie(%map, 'DB_File', $uris_dbm.".db", O_RDONLY, 0664);
+print "Please contact me at: <URL:", $d->url, ">\n";
+print "helm_dir: $helm_dir\n";
+print "urls_of_uris.db: $uris_dbm.db\n";
+$SIG{CHLD} = "IGNORE"; # do not accumulate defunct processes
+while (my $c = $d->accept) {
+ if (fork() == 0) {
+    while (my $r = $c->get_request) {
+        #CSC: mancano i controlli di sicurezza
+        
+        $cont = "";
+        my $cicuri = $r->url; 
+        $cicuri =~ s/^[^?]*\?url=(.*)/$1/;
+        print "*".$r->url."\n";
+        my $http_method = $r->method;
+        my $http_path = $r->url->path;
+        if ($http_method eq 'GET' and $http_path eq "/get") {
+            my $filename = $cicuri;
+            $filename =~ s/cic:(.*)/$1/;
+            $filename =~ s/theory:(.*)/$1/;
+            $filename = $helm_dir.$filename.".xml";
+            my $resolved = $map{$cicuri};
+            print "$cicuri ==> $resolved ($filename)\n";
+            if (stat($filename)) {
+               print "Using local copy\n";
+               open(FD, $filename);
+               while(<FD>) { $cont .= $_; }
+               close(FD);
+               my $res = new HTTP::Response;
+               $res->content($cont);
+               $c->send_response($res);
+            } else {
+               print "Downloading\n";
+               $ua = LWP::UserAgent->new;
+               $request = HTTP::Request->new(GET => "$resolved");
+               $response = $ua->request($request, \&callback);
+               
+               print "Storing file\n";
+               mkdirs($filename);
+               open(FD, ">".$filename);
+               print FD $cont;
+               close(FD);
+
+               my $res = new HTTP::Response;
+               $res->content($cont);
+               $c->send_response($res);
+            }
+        } elsif ($http_method eq 'GET' and $http_path eq "/annotate") {
+            my $do_annotate = ($cicuri =~ /\.ann$/);
+            my $target_to_annotate = $cicuri;
+            $target_to_annotate =~ s/(.*)\.ann$/$1/ if $do_annotate;
+            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/(.*)\.ann$/$1.xml/ if $do_annotate;
+            my $resolved = $map{$cicuri};
+            my $resolved_target = $map{$target_to_annotate} if $do_annotate;
+            if ($do_annotate) {
+               print "($cicuri, $target_to_annotate) ==> ($resolved + $resolved_target) ($filename)\n";
+            } else {
+               print "$cicuri ==> $resolved ($filename)\n";
+            }
+
+            # Retrieves the annotation
+
+            if (stat($filename)) {
+               print "Using local copy for the annotation\n";
+               open(FD, $filename);
+               while(<FD>) { $cont .= $_; }
+               close(FD);
+            } else {
+               print "Downloading the annotation\n";
+               $ua = LWP::UserAgent->new;
+               $request = HTTP::Request->new(GET => "$resolved");
+               $response = $ua->request($request, \&callback);
+               
+               print "Storing file for the annotation\n";
+               mkdirs($filename);
+               open(FD, ">".$filename);
+               print FD $cont;
+               close(FD);
+            }
+            my $annotation = $cont;
+
+            # Retrieves the target to annotate
+
+            $cont = "";
+            if ($do_annotate) {
+               if (stat($filename_target)) {
+                  print "Using local copy for the file to annotate\n";
+                  open(FD, $filename_target);
+                  while(<FD>) { $cont .= $_; }
+                  close(FD);
+               } else {
+                  print "Downloading the file to annotate\n";
+                  $ua = LWP::UserAgent->new;
+                  $request = HTTP::Request->new(GET => "$resolved_target");
+                  $response = $ua->request($request, \&callback);
+               
+                  print "Storing file for the file to annotate\n";
+                  mkdirs($filename_target);
+                  open(FD, ">".$filename_target);
+                  print FD $cont;
+                  close(FD);
+               }
+            }
+            my $target = $cont;
+
+            # Merging the annotation and the target
+
+            $target =~ s/<\?xml [^?]*\?>//sg;
+            $target =~ s/<!DOCTYPE [^>]*>//sg;
+            $annotation =~ s/<\?xml [^?]*\?>//sg;
+            $annotation =~ s/<!DOCTYPE [^>]*>//sg;
+            my $merged = <<EOT;
+<?xml version="1.0" encoding="UTF-8"?>
+<cicxml uri="$target_to_annotate">
+$target
+$annotation
+</cicxml>
+EOT
+
+            # Answering the client
+
+            my $res = new HTTP::Response;
+            $res->content($merged);
+            $c->send_response($res);
+        } elsif ($http_method eq 'GET' and $http_path eq "/getwithtypes") {
+            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;
+            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";
+            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" 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";
+            }
+
+            # Retrieves the annotation
+
+            if (stat($filename)) {
+               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" 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" if ($mode eq "types");
+               print "Storing file for the ann\n" if ($mode eq "ann");
+               mkdirs($filename);
+               open(FD, ">".$filename);
+               print FD $cont;
+               close(FD);
+            }
+            my $annotation = $cont;
+
+            # Retrieves the target to annotate
+
+            $cont = "";
+            my $target;
+            if ($do_annotate) {
+               if (stat($filename_target)) {
+                  print "Using local copy for the file to type\n";
+                  open(FD, $filename_target);
+                  while(<FD>) { $cont .= $_; }
+                  close(FD);
+               } else {
+                  print "Downloading the file to type\n";
+                  $ua = LWP::UserAgent->new;
+                  $request = HTTP::Request->new(GET => "$resolved_target");
+                  $response = $ua->request($request, \&callback);
+               
+                  print "Storing file for the file to type\n";
+                  mkdirs($filename_target);
+                  open(FD, ">".$filename_target);
+                  print FD $cont;
+                  close(FD);
+               }
+               $target = $cont;
+            } else {
+               $target = $annotation;
+               $annotation = "";
+            }
+
+            # Merging the annotation and the target
+
+            $target =~ s/<\?xml [^?]*\?>//sg;
+            $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
+$element
+$annotation
+$endelement
+</cicxml>
+EOT
+
+            # Answering the client
+
+            my $res = new HTTP::Response;
+            $res->content($merged);
+            $c->send_response($res);
+         } elsif ($http_method eq 'GET' and $http_path eq "/getdtd") {
+            my $filename = $cicuri;
+            $filename = $helm_dir."/dtd/".$filename;
+            print "DTD: $cicuri ==> ($filename)\n";
+            if (stat($filename)) {
+               print "Using local copy\n";
+               open(FD, $filename);
+               while(<FD>) { $cont .= $_; }
+               close(FD);
+               my $res = new HTTP::Response;
+               $res->content($cont);
+               $c->send_response($res);
+            } else {
+               die "Could not find DTD!";
+            }
+        } elsif ($http_method eq 'GET' and $http_path eq "/conf") {
+            my $quoted_html_link = $html_link;
+            $quoted_html_link =~ s/&/&amp;/g;
+            $quoted_html_link =~ s/</&lt;/g;
+            $quoted_html_link =~ s/>/&gt;/g;
+            $quoted_html_link =~ s/'/&apos;/g;
+            $quoted_html_link =~ s/"/&quot;/g;
+            print "Configuration requested, returned #$quoted_html_link#\n";
+	    $cont = "<?xml version=\"1.0\"?><html_link>$quoted_html_link</html_link>";
+            my $res = new HTTP::Response;
+            $res->content($cont);
+            $c->send_response($res);
+        } else {
+            print "INVALID REQUEST!!!!!\n";
+            $c->send_error(RC_FORBIDDEN)
+        }
+    }
+    $c->close;
+    undef($c);
+    print "\nCONNECTION CLOSED\n\n";
+    exit;
+  } # fork
+}
+
+#================================
+
+sub callback
+{
+ my ($data) = @_;
+ $cont .= $data;
+}
+
+# Does not raise errors if could not create dirs/files
+
+# Too much powerful: creates even /home, /home/users/, ...
+sub mkdirs
+{
+ my ($pathname) = @_;
+ my @dirs = split /\//,$pathname;
+ my $tmp;
+ foreach $dir (@dirs) {
+  $tmp = ((defined($tmp)) ?  $tmp = $tmp."\/".$dir : "");
+  mkdir($tmp,0777);
+ }
+ rmdir($tmp);
+}