From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2001 16:05:57 +0000 (+0000)
Subject: New online interface
X-Git-Tag: v0_1_2~96
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=64d3512db52983e2a267bf3f4542b5cf2bad225d;p=helm.git

New online interface
---

diff --git a/helm/cgi/mkindex.pl b/helm/cgi/mkindex.pl
index 1b912964b..cd6e47d61 100755
--- a/helm/cgi/mkindex.pl
+++ b/helm/cgi/mkindex.pl
@@ -14,116 +14,15 @@ if (defined ($HELM_LIB_DIR)) {
 # 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";
+#use URI::Escape;
+use CGI;
 
-# LUCA
-# the following lines precompute some escaped string so that they can
-# be used safely in a URI as value for parameters.
+$cgi = new CGI($ENV{"REQUEST_URL"});
 
-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 = $library_dir_on_line.$dirname;
-
-$baseuri0 =~ s/$helm_url_path//;
-
-opendir(DIR, $dirname);
-@filenames = readdir(DIR);
-closedir(DIR);
-
-$output = "";
-foreach $i (@filenames) {
-   if ($i eq "..") {
-      $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/back.gif" alt="[BACK]"></td>
-<td><a href="$uri$i">Parent Directory</a></td>
-</tr>
-EOT
-   } elsif ($i !~ /^\./) {
-      # hidden files excluded
-      (undef,undef,$mode) = stat("$dirname$i");
-      if ($mode &= 16384) {
-         # directory
-         $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/folder.gif" alt="[DIR]"></td>
-<td><a href="$uri$i">$i</a></td>
-</tr>
-EOT
-      } else {
-	 # file
-	 if ($i =~ /\.(con|var|ind)(\.types)?\.xml(\.gz)?$/) {
-            my $i_without_xml = $i;
-            $i_without_xml =~ s/(.*)\.xml(\.gz)/$1/;
-	    # cic file
-            my $baseuri = "cic:".$baseuri0;
-            $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
-<td><a href="$uri$i">$i</a></td>
-<td><a href="$processor_url/apply?key=C1&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML Content</a></td>
-<td><a href="$processor_url/apply?key=C1&key=C2&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML Presentation</a></td>
-<!--
-<td><a href="$processor_url/apply?key=C1&key=C2&key=R2A&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML P Abs</a></td>
--->
-<td><a href="$processor_url/apply?$html_keys&param.getterURL=$esc_getter_url&param.processorURL=$esc_processor_url&param.keys=$esc_html_keys&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">HTML</a></td>
-</tr>
-EOT
-	 } 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(\.gz)/$1/;
-            $i_without_ann_and_xml =~ s/(.*)\.ann\.xml/$1/;
-	    # cic file
-            my $baseuri = "cic:".$baseuri0;
-            $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/text.gif" alt="[DIR]"></td>
-<td><a href="$uri$i">$i</a></td>
-<td><a href="$processor_url/apply?key=C1&xmluri=$esc_getter_url_get_uri$baseuri$i_without_ann_and_xml&annuri=$baseuri$i_without_xml">MathML Content</a></td>
-<td><a href="$processor_url/apply?key=C1&key=C2&xmluri=$esc_getter_url_get_uri$baseuri$i_without_ann_and_xml&annuri=$baseuri$i_without_xml">MathML Presentation</a></td>
-<!--
-<td><a href="$processor_url/apply?key=C1&key=C2&key=R2A&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML P Abs</a></td>
--->
-<td><a href="$processor_url/apply$html_keys&param.getterURL=$esc_getter_url&param.processorURL=$esc_processor_url&param.keys=$esc_html_keys&xmluri=$esc_getter_url_get_uri$baseuri$i_without_ann_and_xml&annuri=$baseuri$i_without_xml">HTML</a></td>
-</tr>
-EOT
-	 } elsif ($i =~ /\.theory\.xml(\.gz)?$/) {
-            my $i_without_xml = $i;
-            $i_without_xml =~ s/(.*)\.xml(\.gz)/$1/;
-	    # theory file
-	    my $baseuri = "theory:".$baseuri0; $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/layout.gif" alt="[DIR]"></td>
-<td><a href="$uri$i">$i</a></td>
-<td><a href="$processor_url/apply?key=T1&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML Content</a></td>
-<td><a href="$processor_url/apply?key=T1&key=T2&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">MathML Presentation</a></td>
-<td><a href="$processor_url/apply?key=T1&key=T2&xmluri=$esc_getter_url_get_uri$baseuri$i_without_xml">HTML</a></td>
-</tr>
-EOT
-         } else {
-	    # other file
-            $output .= <<EOT;
-<tr>
-<td><img border="0" src="/icons/unknown.gif" alt="[DIR]"></td>
-<td><a href="$uri$i">$i</a></td>
-</tr>
-EOT
-	 }
-      }
-   }
-}
+$mode      = $cgi->param('mode');
+$cicuri    = $cgi->param('cicuri');
+$theoryuri = $cgi->param('theoryuri');
+$topurl    = $cgi->url();
 
 print <<EOT;
 Content-type: text/html
@@ -132,17 +31,20 @@ Content-type: text/html
 "http://www.w3.org/TR/REC-html40/loose.dtd">
 <html>
 <head>
-<title>Index of $uri</title>
+ <title>Index of $cicuri and $theoryuri</title>
 </head>
-<body bgcolor="#ffffff" text="#000000">
-<table><tr><td bgcolor="#ffffff" class="title">
-<font size="+3" face="Helvetica,Arial,sans-serif"><b>Index of $uri</b></font>
-</td></tr></table>
-<hr noshade align="left" width="80%">
-<table>
-$output
-</table>
-<hr noshade align="left" width="80%">
-</body>
+<frameset rows="18%,*" border="0" scrolling="no">
+  <frame src="mkcontrol.pl?topurl=$topurl&mode=$mode&cicuri=$cicuri&theoryuri=$theoryuri" name="control"/>
+  <frameset cols="50%,50%" border="0" scrolling="no">
+     <frameset rows="11%,*" border="0" scrolling="no">
+        <frame src="mkheader.pl?uri=$theoryuri" name="theoryheader"/>
+        <frame src="mkindextheory.pl?theoryuri=$theoryuri" name="theoryresult"/>
+     </frameset>
+     <frameset rows="11%,*" border="0" scrolling="no">
+        <frame src="mkheader.pl?uri=$cicuri" name="cicheader"/>
+        <frame src="mkindexcic.pl?cicuri=$cicuri" name="cicresult"/>
+     </frameset>
+  </frameset>
+</frameset>
 </html>
 EOT