Fixed bug in VernacExtend printing + missing vernacular printing rules +

revival of option -translate as a -beautify option.

PS: compilation checked against 11610.



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

1 files changed, 52 insertions, 0 deletions

diff --git a/tools/beautify-archive b/tools/beautify-archive
new file mode 100644
index 0000000000..aac6f3e0e5
--- /dev/null
+++ b/tools/beautify-archive
@@ -0,0 +1,52 @@
+#!/bin/sh
+
+#This script compiles and beautifies an archive, check the correctness
+#of beautified files, then replace the original files by the
+#beautified ones, keeping a copy of original files in $OLDARCHIVE.
+#The script assumes:
+#- that the archive provides a Makefile built by coq_makefile,
+#- that coqc is in the path or that variables COQTOP and COQBIN are set.
+
+OLDARCHIVE=old_files
+NEWARCHIVE=beautify_files
+BEAUTIFYSUFFIX=.beautified
+
+if [ -e $OLDARCHIVE ]; then
+  echo "Warning: $OLDARCHIVE directory found, the files are maybe already beautified";
+  sleep 5;
+fi
+echo ---- Producing beautified files in the beautification directory -------
+if [ -e $NEWARCHIVE ]; then rm -r $NEWARCHIVE; fi
+if [ -e /tmp/$OLDARCHIVE.$$ ]; then rm -r /tmp/$OLDARCHIVE.$$; fi
+cp -pr . /tmp/$OLDARCHIVE.$$
+cp -pr /tmp/$OLDARCHIVE.$$ $NEWARCHIVE
+cd $NEWARCHIVE
+rm description || true
+make clean
+make COQFLAGS='-beautify -q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)' || \
+ { echo ---- Failed to beautify; exit 1; }
+echo -------- Upgrading files in the beautification directory --------------
+beaufiles=`find . -name \*.v$BEAUTIFYSUFFIX`
+for i in $beaufiles; do
+  j=`dirname $i`/`basename $i .v$BEAUTIFYSUFFIX`.v
+  echo Upgrading $j in the beautification directory
+  mv -u -f $i $j
+done
+echo ---- Recompiling beautified files in the beautification directory -----
+make clean
+make || { echo ---- Failed to recompile; exit 1; }
+echo ----- Saving old files in directory $OLDARCHIVE -------------------------
+/bin/rm -r ../$OLDARCHIVE
+mv /tmp/$OLDARCHIVE.$$ ../$OLDARCHIVE
+echo Saving $OLDARCHIVE files done
+echo --------- Upgrading files in current directory ------------------------
+vfiles=`find . -name \*.v`
+cd ..
+for i in $vfiles; do
+  echo Upgrading $i in current directory
+  mv -u -f $NEWARCHIVE/$i $i
+done
+echo -------- Beautification completed -------------------------------------
+echo Old files are in directory '"$OLDARCHIVE"'
+echo New files are in current directory
+echo You can now remove the beautification directory '"$NEWARCHIVE"'