path: root/doc/TP1_files/main.js

/*
  Scripts for my professional web-site: http://www.di.ens.fr/~mine
  Copyright (C) Antoine Miné 2011.
 */


/* main menu */
var options = [
    ["img",  "antoine_mini.png", "80%",   "" ],
    ["Antoine Miné", "", "", "" ],
    ["br"],
    ["Home",         "Accueil",      "index", "" ],
    ["News",         "Nouvelles",    "index", "#news" ],
    ["Research",     "Recherche",    "index", "#research" ],
    ["Habilitation", "Habilitation", "hdr/index", "", "" ],
    ["Ph.D",         "Thèse",        "these/index", "" ],
    ["Projects",     "Projets",      "projects", "" ],
    ["Conferences",  "Conférences",  "confs", "", ],
    ["Software",     "Logiciels",    "index", "#soft", ],
    ["Publications", "Publications", "publications", "", "important" ],
    ["Talks",        "Exposés",      "talks", "" ],
    ["Teaching",     "Enseignement", "index", "#teach", ],
    ["Emulation",    "Émulation",    "emulation", "" ],
    ["Contact",      "Contact",      "index", "#contact" ],
    ["-"],
/*
    ["SAS 2012",     "",   "http://www.sas2012.ens.fr", "", "important" ],
    ["SSCPS 2012",   "",   "http://www.sscps.net", ""],
    ["SAS 2013",     "",  "http://research.microsoft.com/en-us/events/sas2013/", ""],
*/
    ["iFM 2014",   "", "http://ifm2014.cs.unibo.it/", ""],
    ["MOVEP 2014", "", "http://movep14.irccyn.ec-nantes.fr/", ""],
    ["TAPAS 2014", "", "http://cs.au.dk/tapas2014", ""],
    ["TASE 2014",  "", "http://www.nudt.edu.cn/tase2014", ""],
    ["POPL 2015",  "", "http://popl.mpi-sws.org/2015/", ""],
    ["-"],

    ["MPRI 2-6 course (M2)",         "Cours MPRI 2-6 (M2)", "http://www.di.ens.fr/~mine/enseignement/mpri/2013-2014", ""],
    ["Semantic course (L3)",         "Cours de sémantique (L3)", "http://www.di.ens.fr/~rival/semverif-2014/", ""],

    ["-"],
    ["AstréeA",      "",    "http://www.astreea.ens.fr", "", "important" ],
    ["Astrée",       "",    "http://www.astree.ens.fr", "" ],
    ["Apron",        "",    "http://apron.cri.ensmp.fr/library", "" ],
    ["-"],
    ["br"],
    ["img", "logo-cnrs.png",  "64",  "http://www.cnrs.fr" ],
    ["br"],
    ["img", "logo-ens.png",   "82",  "http://www.ens.fr" ],
    ["br"],
    ["img", "logo-inria.png", "128",  "http://www.inria.fr" ],
];

function print_menu(base,here)
{
    for (var i=0; i<options.length; i++) {
        if (options[i][0] == "-")
            document.write("<div class=\"menuspace\"></div>\n");

        else if (options[i][0] == "br")
            document.write("<br>\n");

        else if (options[i][0] == "img") {
            document.write("<div class=\"icon\">");
            if (options[i][3] != "")
                document.write("<a href=\"" + options[i][3] + "\" class=\"noborder\">");
            document.write("<img src=\"" + base + options[i][1] + "\" alt=\"[" + 
                           options[i][1] + "]\" width=\"" + options[i][2] + "\">");
            if (options[i][3] != "")
                document.write("</a>");
            document.write("</div>\n");
        }

        else {
            document.write("<div class=\"menuitem\">");
            var url = options[i][2];
            if (url != "" && url.indexOf(".") == -1) url = url + ".html." + lang + options[i][3];
            if (url != "" && url.indexOf(":") == -1) url = base + url;
            if (options[i][0] == here || url=="") document.write("<b>");
            else if (4 in options[i]) document.write("<a href=\"" + url + "\" class=\"" + options[i][4] + "\">");
            else document.write("<a href=\"" + url + "\">");
            document.write(options[i][ options[i][1]=="" || lang!="fr" ? 0 : 1]);
            if (options[i][0] == here || url=="") document.write("</b>");
            else document.write("</a>");
            document.write("</div>\n");
        }
    }
}

function print_ref(s) 
{ 
    document.write("<a href=\"publications.html." + lang + "#" + s + "\">");
    document.write("<span class=\"pref\">[" + s + "]</span>");
    document.write("</a>");
}

function mailchar(m,i)
{
    var c = "";
    switch (i) {
    case 0: c = 'm'; break;
    case 1: c = 'i'; break;
    case 2: c = 'n'; break;
    case 3: c = 'e'; break;
    case 4: c = '@'; break;
    case 5: c = 'd'; break;
    case 6: c = 'i'; break;
    case 7: c = '.'; break;
    case 8: c = 'e'; break;
    case 9: c = 'n'; break;
    case 10: c = 's'; break;
    case 11: c = '.'; break;
    case 12: c = 'f'; break;
    case 13: c = 'r'; break;
    }
    if (c != "") m.innerHTML = m.innerHTML + "<span>" + c + "</span>";
    if (i<13) setTimeout(function () { mailchar(m,i+1); }, 100 + 100 * Math.random());
}

function main()
{
    var m = document.getElementsByName("mail");
    for (var i=0; i<m.length; i++) {
        mailchar(m[i],0);
    }
}