]> matita.cs.unibo.it Git - helm.git/commitdiff
New on-line interface
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2001 16:06:36 +0000 (16:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2001 16:06:36 +0000 (16:06 +0000)
helm/cgi/mkcontrol.pl [new file with mode: 0755]
helm/cgi/mkheader.pl [new file with mode: 0755]
helm/cgi/mkindexcic.pl [new file with mode: 0755]
helm/cgi/mkindextheory.pl [new file with mode: 0755]

diff --git a/helm/cgi/mkcontrol.pl b/helm/cgi/mkcontrol.pl
new file mode 100755 (executable)
index 0000000..6e593d7
--- /dev/null
@@ -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 <<EOT;
+Content-type: text/html
+
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html>
+<head>
+<title>Control panel</title>
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+</script>
+</head>
+<body bgcolor="#ffffff" text="#000000">
+<form>
+<table>
+  <tr>
+    <td>
+      <b>Format</b>:
+    </td>
+    <td>
+      <select name="output" onChange="updateOutput(this,document.forms[0].format)">
+        <option value="processed" $format_processed>Processed</option>
+        <option value="raw" $format_raw>Raw</option>
+      </select>
+    </td>
+    <td>
+      <select name="format" onChange="updateFormat(this)">
+EOT
+    if ($mode1 eq "raw") {
+       $tmp = "output_".$mode2;
+       $$tmp="selected";
+       print <<EOT;
+        <option value="cic" $output_cic>CIC</option>
+        <option value="zcic" $output_zcic>CIC GZipped</option>
+EOT
+    } else {
+       $tmp = "output_".$mode3;
+       $$tmp="selected";
+       print <<EOT;
+        <option value="html" $output_html>HTML</option>
+        <option value="mml_cont" $output_mml_cont>MathML Content</option>
+        <option value="mml_pres" $output_mml_pres>MathML Presentation</option>
+EOT
+    }
+print <<EOT;
+      </select>
+    </td>
+    <td>
+     <a target="_top" href="$topurl?mode=$mode&cicuri=$cicuri&theoryuri=$theoryuri">Reload</a><br>
+     (do it also before attempting to take a link to the current page)
+     <input type="hidden" name="hiddentopurl" value="$topurl">
+     <input type="hidden" name="hiddenmode" value="$mode">
+     <input type="hidden" name="hiddencicuri" value="$cicuri">
+     <input type="hidden" name="hiddentheoryuri" value="$theoryuri">
+    </td>
+  </tr>
+  <tr>
+    <td colspan="3">
+      <input type="checkbox" $natural onClick="updateNatural(this)">&nbsp;Natural Language</input>
+      <input type="checkbox" $annotations onClick="updateAnnotations(this)">&nbsp;Annotations</input>
+    </td>
+  </tr>
+</table>
+</form>
+</body>
+</html>
+EOT
diff --git a/helm/cgi/mkheader.pl b/helm/cgi/mkheader.pl
new file mode 100755 (executable)
index 0000000..a8e9975
--- /dev/null
@@ -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 <<EOT;
+Content-type: text/html
+
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html>
+<head>
+<title>Control panel</title>
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+</script>
+</head>
+<body bgcolor="#ffffff" text="#000000">
+<table width="100%">
+<tr>
+ <td width="50%">
+  <font size="+3" face="Helvetica,Arial,sans-serif"><b>Index of $uri</b></font>
+  <hr noshade align="left" width="80%">
+ </td>
+</tr>
+</table>
+</body>
+</html>
+EOT
diff --git a/helm/cgi/mkindexcic.pl b/helm/cgi/mkindexcic.pl
new file mode 100755 (executable)
index 0000000..6f816d3
--- /dev/null
@@ -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 = <<EOT;
+<tr>
+<td><img border="0" src="/icons/back.gif" alt="[BACK]"></td>
+<td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddencicuri.value='$uridotdot'; refreshReload(); refreshCICHeader(); this.search='?cicuri=$uridotdot';" onMouseOver="window.status='$uridotdot'; return true">Parent Directory</a></td>
+</tr>
+EOT
+}
+
+foreach $i (@filenames) {
+   my ($type,$name) = split(/,/, $i);
+   if ($type eq "dir") {
+      $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/folder.gif" alt="[DIR]"></td>
+<td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddencicuri.value='$uri$name'; refreshReload(); refreshCICHeader(); this.search='?cicuri=$uri$name';" onMouseOver="window.status='$uri$name'; return true">$name</a></td>
+</tr>
+</tr>
+EOT
+   } elsif ($type eq "object") {
+        if ($name =~ /\.(con|var|ind)(\.types)?$/) {
+           # cic file
+            $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
+<td><a href="" target="cic" onClick="this.href=makeURL('cic','$uri$name','$processor_url','$getter_url')" onMouseOver="window.status='$uri$name'; return true">$name</a>
+</tr>
+EOT
+        } elsif ($name =~ /\.(con|var|ind)\.ann$/) {
+            my $name_without_ann = $name;
+            $name_without_ann_and_xml =~ s/(.*)\.ann/$1/;
+           # cic file
+            $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
+<td><a href="" target="cic" onClick="this.href=makeURL('cic','$uri$name_without_ann&annuri=$uri$name','$processor_url','$getter_url')" onMouseOver="window.status='$uri$name'; return true">$name</a>
+</tr>
+EOT
+         } else {
+            $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/unknown.gif" alt="[DIR]"></td>
+<td>$name</td>
+</tr>
+EOT
+        }
+   } else {
+      $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/burst.gif" alt="[DIR]"></td>
+<td>$name</td>
+</tr>
+EOT
+   }
+}
+
+print <<EOT;
+Content-type: text/html
+
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html>
+<head>
+<title>Index of $uri</title>
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+</script>
+</head>
+<body bgcolor="#ffffff" text="#000000">
+<table>
+$output
+</table>
+<hr noshade align="left" width="80%">
+</body>
+</html>
+EOT
+
+#================================
+
+sub callback
+{
+ my ($data) = @_;
+ $cont .= $data;
+}
diff --git a/helm/cgi/mkindextheory.pl b/helm/cgi/mkindextheory.pl
new file mode 100755 (executable)
index 0000000..fc203ff
--- /dev/null
@@ -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 = <<EOT;
+<tr>
+<td><img border="0" src="/icons/back.gif" alt="[BACK]"></td>
+<td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddentheoryuri.value='$uridotdot'; refreshReload(); refreshTheoryHeader(); this.search='?theoryuri=$uridotdot';" onMouseOver="window.status='$uridotdot'; return true">Parent Directory</a></td>
+</tr>
+EOT
+}
+
+foreach $i (@filenames) {
+   my ($type,$name) = split(/,/, $i);
+   if ($type eq "dir") {
+      $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/folder.gif" alt="[DIR]"></td>
+<td><a href="$myurl" onClick="top.frames[0].document.forms[0].hiddentheoryuri.value='$uri$name'; refreshReload(); refreshTheoryHeader(); this.search='?theoryuri=$uri$name';" onMouseOver="window.status='$uri$name'; return true">$name</a></td>
+</tr>
+EOT
+   } elsif ($type eq "object") {
+        if ($name =~ /\.theory$/) {
+           # theory file
+           $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/generic.red.gif" alt="[DIR]"></td>
+<td><a href="" target="theory" onClick="this.href=makeURL('theory','$uri$name','$processor_url','$getter_url')" onMouseOver="window.status='$uri$name'; return true">$name</a>
+</tr>
+EOT
+         } else {
+            $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/unknown.gif" alt="[DIR]"></td>
+<td>$name</td>
+</tr>
+EOT
+        }
+   } else {
+      $output .= <<EOT;
+<tr>
+<td><img border="0" src="/icons/burst.gif" alt="[DIR]"></td>
+<td>$name</td>
+</tr>
+EOT
+   }
+}
+
+print <<EOT;
+Content-type: text/html
+
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN"
+"http://www.w3.org/TR/REC-html40/loose.dtd">
+<html>
+<head>
+<title>Index of $uri</title>
+<script language="JavaScript" src="http://phd.cs.unibo.it/helm/library3/control.js">
+</script>
+</head>
+<body bgcolor="#ffffff" text="#000000">
+<table>
+$output
+</table>
+<hr noshade align="left" width="80%">
+</body>
+</html>
+EOT
+
+#================================
+
+sub callback
+{
+ my ($data) = @_;
+ $cont .= $data;
+}