Code source du fichier genmenusrc.php

<?php
    // génération du menu de gauche pour les fichiers source du site

    function genmenusrc ($fichier, $menu)
    {
        // sélection du type de menu en fonction de son numéro
        switch ($menu)
        {
            case 1 : $typemenu = "src-php";
                     break;

            case 2 : $typemenu = "src-html";
                     break;

            case 3 : $typemenu = "src-c";
                     break;

            default: $typemenu = "srcdoc";
        }

        // chemin d'accès au fichier contenant le menu
        $ficmenu = DIR_MENUS."/menu-".$typemenu;

        // générer une première ligne du menu appropriée
        if ($menu > 0)
        {
            echo '    <a href="voir.php?page=sources">';
            echo "Code source des fichiers du site</a><br>\n";
        }
        else
        {
            echo '    <a href="voir.php?page=sourcedoc">';
            echo "Code source de la documentation du site</a><br>\n";
        }

        // ligne blanche dans le menu
        echo "    <br>\n";

        // 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)
            {
                // pour l'indentation
                echo "    ";

                // supprimer le passage à la ligne
                $ligne = trim ($ligne);

                // si ligne non vide
                if ($ligne)
                {
                    // traitement différencié en fonction du premier caractère de la ligne
                    switch ($ligne [0])
                    {
                        case "#" : // ligne à afficher en caractères gras
                                   echo "<b>".substr ($ligne, strpos ($ligne, " "))."</b>";
                                   break;

                        case ">" : // nouveau menu
                                   $menulien = $ligne [1];

                                   // essayer de trouver le fichier correspondant dans l'autre menu
                                   if ($menulien == 1 && strpos ($fichier, ".html"))
                                       $fichlien = str_replace (".html", ".php", basename ($fichier));
                                   else if ($menulien == 2 && strpos ($fichier, ".php"))
                                       $fichlien = DIR_PAGES."/".str_replace (".php", ".html", $fichier);

                                   // si ce fichier n'existe pas
                                   if (! file_exists ($fichlien))
                                       // on garde le précédent
                                       $fichlien = $fichier;

                                   // afficher la page avec un autre menu
                                   $lien = "voirsource.php?page=".$fichlien."&menu=".$menulien;

                                   $nomlien = trim (substr ($ligne, 3));

                                   // générer une ligne avec l'appel du lien
                                   echo '<b><a href="'.$lien.'">'.$nomlien."</a></b>";
                                   break;

                        default  : // lien php
                                   // nom du fichier à afficher
                                   $nomlien = basename ($ligne);

                                   // si ce n'est pas celui de la page courante
                                   if ($nomlien !=  basename ($fichier))
                                   {
                                       // on affichera le code source du fichier
                                       $lien = "voirsource.php?page=".$ligne."&menu=".$menu;

                                       // générer une ligne avec l'appel du lien
                                       echo '<a href="'.$lien.'">'.$nomlien."</a>";
                                   }
                                   // sinon
                                   else
                                       // générer le nom du lien dans une autre couleur
                                       echo '<font color="#ff8000">'.$nomlien."</font>";
                    }
                }

                // 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";
    }
?>