Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Improved synchronisation of stdlib index page with current library st…

…ate.

- Made generation of index page fail if a file is missing in list or
  listed but unbound in existing theories
- Added a file hidden-files to optionally list library files not to show
  in the index page (though it is currently empty)
- Added directory Unicode (why not to have it after all?)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
commit f7dba1c53fec7fe7ecefc4758e5a39c0010118b6 1 parent a55947f
herbelin authored
View
2  Makefile.doc
@@ -218,7 +218,7 @@ doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO)
endif
doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
- ./doc/stdlib/make-library-index doc/stdlib/index-list.html
+ ./doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files
doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
cat doc/stdlib/index-list.html > $@
View
1  doc/stdlib/hidden-files
@@ -0,0 +1 @@
+
View
7 doc/stdlib/index-list.html.template
@@ -588,4 +588,11 @@ through the <tt>Require Import</tt> command.</p>
theories/Program/Combinators.v
</dd>
+ <dt> <b>Unicode</b>:
+ Unicode-based notations
+ </dt>
+ <dd>
+ theories/Unicode/Utf8_core.v
+ theories/Unicode/Utf8.v
+ </dd>
</dl>
View
34 doc/stdlib/make-library-index
@@ -3,37 +3,55 @@
# Instantiate links to library files in index template
FILE=$1
+HIDDEN=$2
cp -f $FILE.template tmp
echo -n Building file index-list.prehtml ...
-LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
+#LIBDIRS="Init Logic Structures Bool Arith PArith NArith ZArith QArith Relations Sets Classes Setoids Lists Vectors Sorting Wellfounded MSets FSets Reals Program Numbers Numbers/Natural/Abstract Numbers/Natural/Peano Numbers/Natural/Binary Numbers/Natural/BigN Numbers/Natural/SpecViaZ Numbers/Integer/Abstract Numbers/Integer/NatPairs Numbers/Integer/Binary Numbers/Integer/SpecViaZ Numbers/Integer/BigZ Numbers/NatInt Numbers/Cyclic/Abstract Numbers/Cyclic/Int31 Numbers/Cyclic/ZModulo Numbers/Cyclic/DoubleCyclic Numbers/Rational/BigQ Numbers/Rational/SpecViaQ Strings"
+LIBDIRS=`find theories/* -type d | sed -e "s:^theories/::"`
for k in $LIBDIRS; do
i=theories/$k
echo $i
d=`basename $i`
- if [ "$d" != "Num" -a "$d" != "CVS" ]; then
+ if [ "$d" != "CVS" ]; then
+ ls $i | grep -q \.v'$'
+ if [ $? = 0 ]; then
for j in $i/*.v; do
b=`basename $j .v`
rm -f tmp2
grep -q theories/$k/$b.v tmp
a=$?
+ grep -q theories/$k/$b.v $HIDDEN
+ h=$?
if [ $a = 0 ]; then
- p=`echo $k | sed 's:/:.:g'`
- sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
- mv -f tmp2 tmp
+ if [ $h = 0 ]; then
+ echo Error: $FILE and $HIDDEN both mention theories/$k/$b.v; exit 1
+ else
+ p=`echo $k | sed 's:/:.:g'`
+ sed -e "s:theories/$k/$b.v:<a href=\"Coq.$p.$b.html\">$b</a>:g" tmp > tmp2
+ mv -f tmp2 tmp
+ fi
else
- echo Warning: theories/$k/$b.v is missing in the template file
- fi
+ if [ $h = 0 ]; then
+ echo Error: theories/$k/$b.v is missing in the template file
+ exit 1
+ else
+ echo Error: none of $FILE and $HIDDEN mention theories/$k/$b.v
+ exit 1
+ fi
+
+ fi
done
+ fi
fi
rm -f tmp2
sed -e "s/#$d#//" tmp > tmp2
mv -f tmp2 tmp
done
a=`grep theories tmp`
-if [ $? = 0 ]; then echo Warning: extra files:; echo $a; fi
+if [ $? = 0 ]; then echo Error: extra files:; echo $a; exit 1; fi
mv tmp $FILE
echo Done
Please sign in to comment.
Something went wrong with that request. Please try again.