From: Claudio Sacerdoti Coen Date: Tue, 6 Mar 2001 16:06:36 +0000 (+0000) Subject: New on-line interface X-Git-Tag: v0_1_2~95 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d122e00855f9f44ac0d268e96cbe7b3dccd04db1;p=helm.git New on-line interface --- diff --git a/helm/cgi/mkcontrol.pl b/helm/cgi/mkcontrol.pl new file mode 100755 index 000000000..6e593d7d8 --- /dev/null +++ b/helm/cgi/mkcontrol.pl @@ -0,0 +1,98 @@ +#!/usr/bin/perl + +# First of all, let's load HELM configuration +use Env; +my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; +# this should be the only fixed constant +my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; +if (defined ($HELM_LIB_DIR)) { + $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; +} else { + $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; +} + +# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm +require $HELM_LIB_PATH; + +use CGI; + +$cgi = new CGI($ENV{"REQUEST_URL"}); +$mode = $cgi->param('mode'); +$cicuri = $cgi->param('cicuri'); +$theoryuri = $cgi->param('theoryuri'); +$topurl = $cgi->param('topurl'); +($mode1,$mode2,$mode3,$mode4,$mode5) = split(/,/, $mode); +$natural = "checked" if ($mode4 eq "yes"); +$annotations = "checked" if ($mode5 eq "yes"); +if ($mode1 eq "raw") { + $format_raw = "selected"; +} else { + $format_processed = "selected"; +} + +print < + + +Control panel + + + +
+ + + + + + + + + + +
+ Format: + + + + + Reload
+ (do it also before attempting to take a link to the current page) + + + + +
+  Natural Language +  Annotations +
+
+ + +EOT diff --git a/helm/cgi/mkheader.pl b/helm/cgi/mkheader.pl new file mode 100755 index 000000000..a8e99754f --- /dev/null +++ b/helm/cgi/mkheader.pl @@ -0,0 +1,44 @@ +#!/usr/bin/perl + +# First of all, let's load HELM configuration +use Env; +my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; +# this should be the only fixed constant +my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; +if (defined ($HELM_LIB_DIR)) { + $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; +} else { + $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; +} + +# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm +require $HELM_LIB_PATH; + +use CGI; + +$cgi = new CGI($ENV{"REQUEST_URL"}); +$uri = $cgi->param('uri'); + +print < + + +Control panel + + + + + + + +
+ Index of $uri +
+
+ + +EOT diff --git a/helm/cgi/mkindexcic.pl b/helm/cgi/mkindexcic.pl new file mode 100755 index 000000000..6f816d327 --- /dev/null +++ b/helm/cgi/mkindexcic.pl @@ -0,0 +1,119 @@ +#!/usr/bin/perl + +# First of all, let's load HELM configuration +use Env; +my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; +# this should be the only fixed constant +my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; +if (defined ($HELM_LIB_DIR)) { + $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; +} else { + $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; +} + +# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm +require $HELM_LIB_PATH; + +use URI::Escape; +use LWP::UserAgent; +use CGI; + +my $cgi = new CGI($ENV{"REQUEST_URL"}); +$uri = $cgi->param('cicuri'); +$uri =~ s/(.*)\/$/$1/; # Remove a final slash if present +$uri .= "/"; # Put a final slash +$myurl = $cgi->url(); + +$cont = ""; # modified by side-effect by &callback +my $ua = LWP::UserAgent->new; +my $request = HTTP::Request->new(GET => $getter_url."ls?format=txt&baseuri=".$uri); +my $response = $ua->request($request, \&callback); + +@filenames = split(/\n/, $cont); + +my $uridotdot = $uri; +$uridotdot =~ s/(.*)\/.+/$1/; +if ($uri ne "cic:/") { + # Let's print the link to the parent directory + $output = < +[BACK] +Parent Directory + +EOT +} + +foreach $i (@filenames) { + my ($type,$name) = split(/,/, $i); + if ($type eq "dir") { + $output .= < +[DIR] +$name + + +EOT + } elsif ($type eq "object") { + if ($name =~ /\.(con|var|ind)(\.types)?$/) { + # cic file + $output .= < +[DIR] +$name + +EOT + } elsif ($name =~ /\.(con|var|ind)\.ann$/) { + my $name_without_ann = $name; + $name_without_ann_and_xml =~ s/(.*)\.ann/$1/; + # cic file + $output .= < +[DIR] +$name + +EOT + } else { + $output .= < +[DIR] +$name + +EOT + } + } else { + $output .= < +[DIR] +$name + +EOT + } +} + +print < + + +Index of $uri + + + + +$output +
+
+ + +EOT + +#================================ + +sub callback +{ + my ($data) = @_; + $cont .= $data; +} diff --git a/helm/cgi/mkindextheory.pl b/helm/cgi/mkindextheory.pl new file mode 100755 index 000000000..fc203ff0f --- /dev/null +++ b/helm/cgi/mkindextheory.pl @@ -0,0 +1,108 @@ +#!/usr/bin/perl + +# First of all, let's load HELM configuration +use Env; +my $HELM_LIB_DIR = $ENV{"HELM_LIB_DIR"}; +# this should be the only fixed constant +my $DEFAULT_HELM_LIB_DIR = "/projects/helm/on-line/local/lib/helm"; +if (defined ($HELM_LIB_DIR)) { + $HELM_LIB_PATH = $HELM_LIB_DIR."/configuration.pl"; +} else { + $HELM_LIB_PATH = $DEFAULT_HELM_LIB_DIR."/configuration.pl"; +} + +# next require defines: $helm_dir, $html_link, $dtd_dir, $uris_dbm +require $HELM_LIB_PATH; + +use URI::Escape; +use LWP::UserAgent; +use CGI; + +my $cgi = new CGI($ENV{"REQUEST_URL"}); +$uri = $cgi->param('theoryuri'); +$uri =~ s/(.*)\/$/$1/; # Remove a final slash if present +$uri .= "/"; # Put a final slash +$myurl = $cgi->url(); + +$cont = ""; # modified by side-effect by &callback +my $ua = LWP::UserAgent->new; +my $request = HTTP::Request->new(GET => $getter_url."ls?format=txt&baseuri=".$uri); +my $response = $ua->request($request, \&callback); + +@filenames = split(/\n/, $cont); + +my $uridotdot = $uri; +$uridotdot =~ s/(.*)\/.+/$1/; +if ($uri ne "theory:/") { + # Let's print the link to the parent directory + $output = < +[BACK] +Parent Directory + +EOT +} + +foreach $i (@filenames) { + my ($type,$name) = split(/,/, $i); + if ($type eq "dir") { + $output .= < +[DIR] +$name + +EOT + } elsif ($type eq "object") { + if ($name =~ /\.theory$/) { + # theory file + $output .= < +[DIR] +$name + +EOT + } else { + $output .= < +[DIR] +$name + +EOT + } + } else { + $output .= < +[DIR] +$name + +EOT + } +} + +print < + + +Index of $uri + + + + +$output +
+
+ + +EOT + +#================================ + +sub callback +{ + my ($data) = @_; + $cont .= $data; +}