From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 6 Mar 2001 18:47:08 +0000 (+0000)
Subject: getter flags considered
X-Git-Tag: v0_1_2~92
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7998b94e5f83fb3c9009762a875a0136bc4052ec;p=helm.git

getter flags considered
---

diff --git a/helm/cgi/mkindexcic.pl b/helm/cgi/mkindexcic.pl
index 0033a512a..e592b0579 100755
--- a/helm/cgi/mkindexcic.pl
+++ b/helm/cgi/mkindexcic.pl
@@ -44,7 +44,10 @@ EOT
 }
 
 foreach $i (@filenames) {
-   my ($type,$name) = split(/,/, $i);
+   my ($type,$name,$flags) = split(/, /, $i);
+   my ($flagscic, $flagstypes) = split(/,/, $flags);
+   $flagscic =~ s/^<(.*)/$1/;
+   $flagstypes =~ s/(.*)>$/$1/;
    if ($type eq "dir") {
       $output .= <<EOT;
 <tr>
@@ -54,22 +57,12 @@ foreach $i (@filenames) {
 </tr>
 EOT
    } elsif ($type eq "object") {
-	 if ($name =~ /\.(con|var|ind)(\.types)?$/) {
+	 if ($name =~ /\.(con|var|ind)$/) {
 	    # 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>
+<td><a href="" target="cic" onClick="this.href=makeURL('cic','$uri$name','$processor_url','$getter_url','$flagscic','$flagstypes')" onMouseOver="window.status='$uri$name'; return true">$name</a>
 </tr>
 EOT
          } else {
diff --git a/helm/cgi/mkindextheory.pl b/helm/cgi/mkindextheory.pl
index 05bb5b925..b92f36361 100755
--- a/helm/cgi/mkindextheory.pl
+++ b/helm/cgi/mkindextheory.pl
@@ -44,7 +44,10 @@ EOT
 }
 
 foreach $i (@filenames) {
-   my ($type,$name) = split(/,/, $i);
+   my ($type,$name,$flags) = split(/, /, $i);
+   my ($flagscic, $flagstypes) = split(/,/, $flags);
+   $flagscic =~ s/^<(.*)/$1/;
+   $flagstypes =~ s/(.*)>$/$1/;
    if ($type eq "dir") {
       $output .= <<EOT;
 <tr>
@@ -58,7 +61,7 @@ EOT
 	    $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>
+<td><a href="" target="theory" onClick="this.href=makeURL('theory','$uri$name','$processor_url','$getter_url','$flagscic','$flagstypes')" onMouseOver="window.status='$uri$name'; return true">$name</a>
 </tr>
 EOT
          } else {