Code source du fichier genmenudoc.php

<?php
    // génération du menu pour les pages de documentation

    function genmenudoc ($page_cour)
    {
        // chemin d'accès au fichier contenant le menu
        $ficmenu = DIR_MENUS."/menu-doc";

        // ouvrir le fichier contenant le menu
        $descmenu = fopen ($ficmenu, "r");

        // si l'ouverture s'est bien passée
        if ($descmenu)
        {
            // lire la première ligne du menu
            $ligne = fgets ($descmenu, LG_MAX_HTML);

            // tant qu'on a pu lire une ligne
            while ($ligne)
            {
                // supprimer le retour à la ligne
                $ligne = trim ($ligne);

                // pour l'indentation
                echo "    ";

                // si la ligne n'est pas vide
                if ($ligne)
                {
                    // rechercher le premier espace dans la ligne
                    $posblanc = strpos ($ligne, " ");

                    // séparer le nom du script php du nom du lien à afficher
                    // ou l'indicateur en début de ligne du texte à afficher
                    $debut = substr ($ligne, 0, $posblanc);
                    $suite = trim (substr ($ligne, $posblanc));

                    // traitement différencié en fonction du premier paramètre
                    switch ($debut)
                    {
                        case "##" : // ligne à afficher en caractères gras agrandis
                                    echo '<font style="font-size:120%"><b>'.$suite."</b></font>";
                                    break;

                        case "#"  : // ligne à afficher en caractères gras
                                    echo "<b>".$suite."</b>";
                                    break;

                        case $page_cour : // page courante affichée en orange
                                    echo '<font color="#ff8000">'.$suite."</font>";
                                    break;

                                    // lien php
                        default   : // si lien vers un script php
                                    if (strpos ($debut, ".php"))
                                        // l'afficher tel quel
                                        echo '<a href="'.$debut.'">'.$suite."</a>";
                                    // sinon
                                    else
                                        // afficher la page de documentation demandée
                                        echo '<a href="voir.php?page='.$debut.'">'.$suite."</a>";
                    }
                }

                // passage à la ligne
                echo "<br>\n";

                // lire la ligne suivante du menu
                $ligne = fgets ($descmenu, LG_MAX_HTML);
            }

            // terminé avec le fichier contenant le menu
            fclose ($descmenu);
        }
        // sinon
        else
            // message d'erreur
            echo "Fichier ".basename ($ficmenu)." manquant";
    }
?>