X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Fgetter%2Fmkindexes.pl;fp=components%2Fgetter%2Fmkindexes.pl;h=3107846aa42f8be37fcb4755c8b7a001401987a6;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1

diff --git a/components/getter/mkindexes.pl b/components/getter/mkindexes.pl
new file mode 100755
index 000000000..3107846aa
--- /dev/null
+++ b/components/getter/mkindexes.pl
@@ -0,0 +1,40 @@
+#!/usr/bin/perl -w
+# To be invoked in a directory where a tree of XML files of the HELM library is
+# rooted. This script will then creates INDEX files in all directories of the
+# tree.
+use strict;
+my $index_fname = "INDEX";
+sub getcwd() {
+  my $pwd = `pwd`;
+  chomp $pwd;
+  return $pwd;
+}
+sub add_trailing_slash($) {
+  my ($dir) = @_;
+  return $dir if ($dir =~ /\/$/);
+  return "$dir/";
+}
+sub indexable($) {
+  my ($fname) = @_;
+  return 1 if ($fname =~ /\.(ind|types|body|var|theory).xml/);
+  return 0;
+}
+my @todo = (getcwd());
+while (my $dir = shift @todo) {
+  print "$dir\n";
+  chdir $dir or die "Can't chdir to $dir\n";
+  open LS, 'ls | sed \'s/\\.gz//\' | sort | uniq |';
+  open INDEX, "> $index_fname"
+    or die "Can't open $index_fname in " . getcwd() .  "\n";
+  while (my $entry = <LS>) {
+    chomp $entry;
+    if (-d $entry) {
+      print INDEX add_trailing_slash($entry) . "\n";
+      push @todo, getcwd() . "/$entry";
+    } else {
+      print INDEX "$entry\n" if indexable($entry);
+    }
+  }
+  close INDEX;
+  close LS;
+}