Scripts de correction d'uri

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1161 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 123 insertions, 0 deletions

diff --git a/contrib/xml/fix_uri.pl b/contrib/xml/fix_uri.pl
new file mode 100755
index 000000000..922121ebc
--- /dev/null
+++ b/contrib/xml/fix_uri.pl
@@ -0,0 +1,120 @@
+#!/usr/bin/perl -w
+
+################################################################################
+#                                                                              #
+#                                PROJECT HELM                                  #
+#                                                                              #
+#                      A tactic to print Coq objects in XML                    #
+#                                                                              #
+#                 Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>                #
+#                                  20/12/2000                                  #
+#                                                                              #
+# This module script takes from stdin two list of uris of xml files containing #
+# uris to each other. The uris in the second list are broken because each uri  #
+# is only the suffix of the right one that appear in the first list.           #
+# The script modifies all the files in the second list fixing the uris.        #
+#                                                                              #
+# Assumptions:                                                                 #
+#  1) no more than one uri per line                                            #
+#  2) all uris have this format: "cic:/section/term"                           #
+#     where there are no "/" in term                                           #
+#                                                                              #
+################################################################################
+
+use strict;
+
+my %name_to_uri;
+
+open(FD1,$ARGV[0]);
+my @Argv = <FD1>;
+close(FD1);
+
+open(FD1,$ARGV[1]);
+my @savedArgv = <FD1>;
+close(FD1);
+
+my @Argv2;
+my $tmpi = 0;
+for (my $i = 0; $i <= $#Argv; $i++) {
+ chomp($Argv[$i]);
+ $Argv[$i] =~ s/^cic:\/(.*)/$1.xml/;
+ $Argv2[$tmpi++] = $Argv[$i] if !($Argv[$i] =~ /^theory:/);
+}
+
+my @savedArgv2;
+$tmpi = 0;
+for (my $i = 0; $i <= $#savedArgv; $i++) {
+ chomp($savedArgv[$i]);
+ $savedArgv[$i] =~ s/^cic:\/(.*)/$1.xml/;
+ $savedArgv2[$tmpi++] = $savedArgv[$i] if !($savedArgv[$i] =~ /^theory:/);
+}
+
+# phase 1: fill %name_to_uri
+
+print "phase 1: collecting uris\n";
+
+for my $i (@Argv2) {
+ if ($i =~ /.*\.(con|ind|var)\.xml/) {
+  my $j = $i;
+  $j =~ s/.*\/(.*)\.xml$/$1/;         # get file name
+  $i =~ s/(\.\/)?(.*)\.xml/$2/;       # get uri
+  my @tmp;
+  if (defined (my $urisref = $name_to_uri{$j}))
+   { @tmp = @$urisref; }
+  else
+   { @tmp = (); }
+  push(@tmp, $i);
+  $name_to_uri{$j} = \@tmp;
+ }
+}
+
+# phase 2: repair the uris in all files
+
+print "phase 2: repairing uris\n";
+
+for my $i (@savedArgv2) {
+print "Processing $i\n";
+ open (FDi, "<$i") or die "critical error: file $i does not exist!\n";
+ open (FDo, ">$i.new") or die "critical error: file $i.new could not be created!\n";
+ while(<FDi>) {
+  if (/"cic:(.*)"/) {
+   my ($origline, $line, $filename) = ($_, $_, $_);
+   chomp ($filename);
+   $filename =~ s/(.*)"cic:([^"]*)"(.*)/$2/;
+   my $section = $filename;
+   $filename =~ s/.*\/(.*)$/$1/;                        # get file name
+   $section  =~ s/(.*)\/(.*)$/$1/;			# get section
+   if (defined (my $urisref = $name_to_uri{$filename})) {
+    my @uris = @$urisref;
+    my $uri;
+    for (my $h = 0; $h <= $#uris; $h++) {
+     my $huri = $uris[$h];
+     if (index("/$huri", "$section/") >= 0) {
+      if (!defined($uri)) {
+       $uri = $huri;
+      } else {
+       print "uri scelta a caso per il termine $filename nel file $i\n";
+       print "la prima scelta era $uri\nla seconda $huri\n";
+       print "la sezione era $section\n\n";
+      }
+     }
+    }
+    if (!defined($uri)) {
+     print "Due to internal error uri which filename is $filename in file $i can't be repaired!\n";
+     $line = $origline;
+    } else {
+     $line =~ s/(.*)"cic:([^"]*)"(.*)/$1"cic:\/$uri"$3/;
+    }
+    print FDo "$line";
+   } else {
+    print "uri which filename is $filename in file $i can't be repaired!\n";
+    print FDo $origline;
+   }
+  } else {
+   print FDo;
+  }
+ }
+ close (FDi);
+ close (FDo);
+ rename("$i.new", "$i");
+}
diff --git a/contrib/xml/mkindex.sh b/contrib/xml/mkindex.sh
new file mode 100755
index 000000000..074eff0bc
--- /dev/null
+++ b/contrib/xml/mkindex.sh
@@ -0,0 +1,3 @@
+#!/bin/bash
+
+echo `find . -name "*.xml"` | uris_of_filenames.pl > index.txt