aboutsummaryrefslogtreecommitdiff
path: root/dev/doc/check-grammar
diff options
context:
space:
mode:
authorherbelin2006-05-23 21:51:59 +0000
committerherbelin2006-05-23 21:51:59 +0000
commite24d8149c3aefd11b03458b6f9b3e38ca454b07a (patch)
tree7c66dda6b63ea0c1f3e6e03259ef0b1609aca8b6 /dev/doc/check-grammar
parentb65fd67d6210f480eed759d58422ca8c4da95eab (diff)
Restructuration dossier dev et mise à jour de certaines documentations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8856 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/doc/check-grammar')
-rwxr-xr-xdev/doc/check-grammar50
1 files changed, 0 insertions, 50 deletions
diff --git a/dev/doc/check-grammar b/dev/doc/check-grammar
deleted file mode 100755
index 67da1bc513..0000000000
--- a/dev/doc/check-grammar
+++ /dev/null
@@ -1,50 +0,0 @@
-#!/bin/bash
-# This scripts checks that the new grammar of Coq as defined in syntax-v8.tex
-# is consistent in the sense that all invoked non-terminals are defined
-
-defined-nt() {
- grep "\\DEFNT{.*}" syntax-v8.tex | sed -e "s|.*DEFNT{\([^}]*\)}.*|\1|"|\
- sort | sort -u
-}
-
-used-nt() {
- cat syntax-v8.tex | tr \\\\ \\n | grep "^NT{.*}" |\
- sed -e "s|^NT{\([^}]*\)}.*|\1|" | egrep -v ^\#1\|non-terminal | sort -u
-}
-
-used-term() {
- cat syntax-v8.tex | tr \\\\ \\n | grep "^TERM{.*}" |\
- sed -e "s|^TERM{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1\|terminal | sort -u
-}
-
-used-kwd() {
- cat syntax-v8.tex | tr \\\\ \\n | grep "^KWD{.*}" |\
- sed -e "s|^KWD{\([^}]*\)}.*|\1|" -e "s|\\$||g" | egrep -v ^\#1 | sort -u
-}
-
-defined-nt > def
-used-nt > use
-used-term > use-t
-used-kwd > use-k
-diff def use > df
-
-###############################
-echo
-if grep ^\> df > /dev/null 2>&1 ; then
- echo Undefined non-terminals:
- echo ========================
- echo
- grep ^\> df | sed -e "s|^> ||"
- echo
-fi
-if grep ^\< df > /dev/null 2>&1 ; then
- echo Unused non-terminals:
- echo =====================
- echo
- grep ^\< df | sed -e "s|^< ||"
- echo
-fi
-#echo Used terminals:
-#echo ===============
-#echo
-#cat use-t \ No newline at end of file