function highlight_num ( $file )
        {
#-k     format html
#-      PHP code highlighter

        echo '<code style="float: left; color: gray; text-align: right; margin-right: 6pt;
                padding-right: 6pt; border-right: 1px solid gray;">',
                implode(range(1, count(file($file))), '<br />'),
                '</code>';
        echo highlight_file($file, true);
        }

?>