Improved synchronisation of stdlib index page with current library state.

- 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

3 files changed, 34 insertions, 8 deletions

diff --git a/doc/stdlib/hidden-files b/doc/stdlib/hidden-files
new file mode 100644
index 000000000..8b1378917
--- /dev/null
+++ b/doc/stdlib/hidden-files
@@ -0,0 +1 @@
+
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index de4b6de94..d688124d0 100644
--- a/doc/stdlib/index-list.html.template
+++ b/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>
diff --git a/doc/stdlib/make-library-index b/doc/stdlib/make-library-index
index 6d3a64a9f..1a70567f6 100755
--- a/doc/stdlib/make-library-index
+++ b/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