]> matita.cs.unibo.it Git - helm.git/commitdiff
Handling of the splitting of constants into body + type.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 10 Oct 2002 15:48:33 +0000 (15:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 10 Oct 2002 15:48:33 +0000 (15:48 +0000)
helm/http_getter/http_getter.pl.in

index bccb61548210885cc454d510fd0067fc134e6b05..9fd957c39952629bb89787d8397b291ffc31ca76 100755 (executable)
@@ -529,9 +529,9 @@ sub finduris { # find uris for cic and theory trees generation
 
     if ($localpart =~ /^[^\/]*$/) { # no slash, an OBJECT
      $basepart = $localpart;
-     $basepart =~ s/^([^.]*\.[^.]*)(\.types)?(\.ann)?/$1/;
-                                              # remove exts .types or
-                                              # .types.ann
+     $basepart =~ s/^([^.]*\.[^.]*)((\.body)|(\.types))?(\.ann)?/$1/;
+                                              # remove exts .types, .body,
+                                              # .types.ann or .body.ann
      $flags = $objects{$basepart}; # get old flags
      if ($localpart =~ /\.ann$/) {
       $flags = add_flag("ann","YES",$flags);
@@ -545,6 +545,13 @@ sub finduris { # find uris for cic and theory trees generation
      } else {
       $flags = add_flag("types","NO",$flags);
      }
+     if ($localpart =~ /\.body$/) {
+      $flags = add_flag("body","YES",$flags);
+     } elsif ($localpart =~ /\.body\.ann$/) {
+      $flags = add_flag("body","ANN",$flags);
+     } else {
+      $flags = add_flag("body","NO",$flags);
+     }
      $objects{$basepart} = $flags; # save new flags
     } else { # exists at least one slash, a DIR
      ($dirname) = split (/\//, $localpart);
@@ -576,9 +583,10 @@ sub finduris { # find uris for cic and theory trees generation
    $content .= "\t<object name=\"$key\">\n";
    $flags = $objects{$key};
    $flags =~ s/^<(.*)>$/$1/;
-   my ($annflag,$typesflag) = split /,/,$flags;
+   my ($annflag,$typesflag,$bodyflag) = split /,/,$flags;
    $content .= "\t\t<ann value=\"$annflag\" />\n";
    $content .= "\t\t<types value=\"$typesflag\" />\n";
+   $content .= "\t\t<body value=\"$bodyflag\" />\n";
    $content .= "\t</object>\n";
   }
   $content .= "</ls>\n";
@@ -589,17 +597,18 @@ sub finduris { # find uris for cic and theory trees generation
 }
 
 sub add_flag {
-# manage string like: "<ann_flag,type_flag>"
+# manage string like: "<ann_flag,type_flag,body_flag>"
 # "ann_flag" may be one of "ann_YES", "ann_NO"
 # "type_flag" may be one of "types_NO", "types_YES", "types_ANN"
+# "body_flag" may be one of "body_NO", "body_YES", "body_ANN"
 # when adding a flag the max between the current flag and the new flag
-# is taken, the orders are ann_NO < ann_YES and types_NO < types_YES <
-# types_ANN
+# is taken, the orders are ann_NO < ann_YES, types_NO < types_YES <
+# types_ANN and body_NO < body_YES < body_ANN
  my ($flagtype,$newflag,$str) = @_;
- $str = "<,>" if ($str eq "");
- ($str =~ s/^<(.*,.*)>$/$1/) or die "Internal error: ".
+ $str = "<,,>" if ($str eq "");
+ ($str =~ s/^<(.*,.*,.*)>$/$1/) or die "Internal error: ".
    "wrong string format for flag adding in $str";
- my ($annflag,$typeflag) = split /,/,$str;
+ my ($annflag,$typeflag,$bodyflag) = split /,/,$str;
  if ($flagtype eq "ann") { # ANN flag handling
   if ($newflag eq "YES") {
    $annflag = "YES";
@@ -619,10 +628,21 @@ sub add_flag {
   } else {
    die "Internal error: typeflag must be \"YES\", \"NO\" or \"ANN\"";
   }
+ } elsif ($flagtype eq "body") { # BODY flag handling
+  if ($newflag eq "ANN") {
+   $bodyflag = "ANN";
+  } elsif ($newflag eq "YES") {
+   $bodyflag = "YES" unless ($bodyflag eq "ANN");
+  } elsif ($newflag eq "NO") {
+   $bodyflag = "NO"
+     unless (($bodyflag eq "ANN") or ($bodyflag eq "YES"));
+  } else {
+   die "Internal error: typeflag must be \"YES\", \"NO\" or \"ANN\"";
+  }
  } else {
   die "Internal error: unsupported flagtype \"$flagtype\"";
  }
- $str = "<$annflag,$typeflag>";
+ $str = "<$annflag,$typeflag,$bodyflag>";
 }
 
 #CSC: Too much powerful: creates even /home, /home/users/, ...