From: Claudio Sacerdoti Coen Date: Thu, 1 Mar 2001 11:27:14 +0000 (+0000) Subject: WebEQ definitely no more used X-Git-Tag: v0_1_2~103 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1092edce200adcf91a8c7f8caf947b3ac6bbbd0d;p=helm.git WebEQ definitely no more used --- diff --git a/helm/cgi/mkindex.pl b/helm/cgi/mkindex.pl index 61c39d0e4..1b912964b 100755 --- a/helm/cgi/mkindex.pl +++ b/helm/cgi/mkindex.pl @@ -1,15 +1,39 @@ #!/usr/bin/perl -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, $dtd_dir, $uris_dbm - require $HELM_CONFIGURATION_PATH; +# 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; + +$getter_url_get_uri = $getter_url."get?uri="; +$html_keys = "key=C1&key=HC2"; + +# LUCA +# the following lines precompute some escaped string so that they can +# be used safely in a URI as value for parameters. + +use URI::Escape; + +#$escape_these = "\;\/\?\:\@\&\=\+\,\$"; +$escape_these = "&=;:?"; +$esc_getter_url = uri_escape($getter_url, $escape_these); +$esc_processor_url = uri_escape($processor_url, $escape_these); +$esc_getter_url_get_uri = uri_escape($getter_url_get_uri, $escape_these); +$esc_html_keys = uri_escape($html_keys, $escape_these); $baseuri0 = $dirname = $uri = $ENV{"REQUEST_URI"}; $dirname =~ s/$helm_url_path//; -$dirname = $helm_dir.$dirname; +$dirname = $library_dir_on_line.$dirname; $baseuri0 =~ s/$helm_url_path//; @@ -21,7 +45,10 @@ $output = ""; foreach $i (@filenames) { if ($i eq "..") { $output .= < Parent Directory + +[BACK] +Parent Directory + EOT } elsif ($i !~ /^\./) { # hidden files excluded @@ -29,43 +56,69 @@ EOT if ($mode &= 16384) { # directory $output .= < $i + +[DIR] +$i + EOT } else { # file - if ($i =~ /\.(con|var|ind)\.xml$/) { + if ($i =~ /\.(con|var|ind)(\.types)?\.xml(\.gz)?$/) { my $i_without_xml = $i; - $i_without_xml =~ s/(.*)\.xml/$1/; + $i_without_xml =~ s/(.*)\.xml(\.gz)/$1/; # cic file my $baseuri = "cic:".$baseuri0; $output .= < $i MathML HTML WEBEQ WEBEQ PRESENTATION ONLY + +[DIR] +$i +MathML Content +MathML Presentation + +HTML + EOT - } elsif ($i =~ /\.(con|var|ind)\.ann\.xml$/) { + } elsif ($i =~ /\.(con|var|ind)\.ann\.xml(\.gz)?$/) { my $i_without_xml = $i; my $i_without_ann_and_xml = $i; - $i_without_xml =~ s/(.*)\.xml/$1/; + $i_without_xml =~ s/(.*)\.xml(\.gz)/$1/; $i_without_ann_and_xml =~ s/(.*)\.ann\.xml/$1/; # cic file my $baseuri = "cic:".$baseuri0; $output .= < $i MathML HTML WEBEQ WEBEQ PRESENTATION ONLY + +[DIR] +$i +MathML Content +MathML Presentation + +HTML + EOT - } elsif ($i =~ /\.theory\.xml$/) { + } elsif ($i =~ /\.theory\.xml(\.gz)?$/) { my $i_without_xml = $i; - $i_without_xml =~ s/(.*)\.xml/$1/; + $i_without_xml =~ s/(.*)\.xml(\.gz)/$1/; # theory file - my $baseuri = "theory:".$baseuri0; - $output .= < $i MathML HTML + my $baseuri = "theory:".$baseuri0; $output .= < +[DIR] +$i +MathML Content +MathML Presentation +HTML + EOT } else { # other file $output .= < $i + +[DIR] +$i + EOT } } @@ -86,9 +139,9 @@ Content-type: text/html Index of $uri
-
+
 $output
-
+

diff --git a/helm/cgi/use_webeqp.pl b/helm/cgi/use_webeqp.pl deleted file mode 100755 index 72bfb1fa0..000000000 --- a/helm/cgi/use_webeqp.pl +++ /dev/null @@ -1,18 +0,0 @@ -#!/usr/bin/perl - -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, $dtd_dir, $uris_dbm - require $HELM_CONFIGURATION_PATH; - -require CGI; - -$q = new CGI; -$uri = $q->param("uri"); - -print <new; -$request = HTTP::Request->new(GET => "$url"); -$response = $ua->request($request, \&callback); - -$content =~ s/\r//sg; -$content =~ s/\n/ /sg; -$content =~ s/]*(.*)>/$1/sg; -$content =~ s/]*>//sg; -$content =~ s/"/'/g; -$content =~ s/&/&/g; - -print < - - -Generato in automatico a partire da $url - - - - - - - - - - -EOT - -#========================= - -sub callback -{ - my ($data) = @_; - $content .= $data; -} diff --git a/helm/cgi/webeqp.pl b/helm/cgi/webeqp.pl deleted file mode 100755 index b4891d325..000000000 --- a/helm/cgi/webeqp.pl +++ /dev/null @@ -1,69 +0,0 @@ -#!/usr/bin/perl - -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, $dtd_dir, $uris_dbm - require $HELM_CONFIGURATION_PATH; - -require HTTP::Request; -require LWP::UserAgent; -use CGI; - -$url = $ENV{"REQUEST_URI"}; -$url =~ s/.*mmlurl=(.*)/$1/; - -$content = ""; - -$ua = LWP::UserAgent->new; -$request = HTTP::Request->new(GET => "$url"); -$response = $ua->request($request, \&callback); - -$content =~ s/\r//sg; -$content =~ s/\n/ /sg; -$content =~ s/]*>//sg; -$content =~ s/<\?xml[^?]*\?>//sg; -$content =~ s/"/'/g; -$content =~ s/&/&/g; -$content =~ s/]*>//sg; -$content =~ s/(<\/?semantics[^>]*>)//sg; -$content =~ s/()/$1 -->/sg; -$content =~ s/([^<]*)<\/mo>/$2<\/mo><\/maction>/sg; -$content =~ s/([^<]*)<\/mi>/$2<\/mi><\/maction>/sg; -$content =~ s/helm:xref='[^']*'//sg; -$content =~ s/xmlns:helm='[^']*'//sg; -$content =~ s/xlink:href='[^']*'//sg; -$content =~ s/xmlns:xlink='[^']*'//sg; -$content =~ s//&$1;/sg; - -print < - - -Generato in automatico a partire da $url - - - - - - - - - - -EOT - -#========================= - -sub callback -{ - my ($data) = @_; - $content .= $data; -}