imported>Mathieu |
imported>Mathieu |
Line 1: |
Line 1: |
− | /* <pre><nowiki> */
| + | <noinclude> |
| + | ==Usage== |
| + | Template use to typeset an event name in an event-b listing. |
| + | ==Example== |
| | | |
− | // [[User:Lupin/popups.js]] - please include this line
| + | {{l_machine|AntiCollide}} |
− | document.write('<script type="text/javascript" src="'
| + | {{l_refines|Safety}} |
− | + 'http://wiki.event-b.org/index.php?title=User:Mathieu/popups.js'
| + | {{l_sees|Network}} |
− | + '&action=raw&ctype=text/javascript&dontcountme=s"></script>');
| + | {{l_component|Acyclic}} |
| + | {{l_variables|v1}} |
| + | {{l_variable|v2}} |
| + | {{l_invariants}} |
| + | {{l_invariant|inv1|v2 ∈ BOOL}} |
| + | {{l_theorems}} |
| + | {{l_theorem|inv1|v2 ∈ BOOL}} |
| + | {{l_events}} |
| + | {{l_event|control|extended|ordinary}} |
| + | {{l_parameters}} |
| + | {{l_param|a}} |
| + | {{l_param|x|y|z}} |
| + | {{l_guards}} |
| + | {{l_guard|grd1|x ⊆ next}} |
| + | {{l_witnesses}} |
| + | {{l_witness|y|y=v}} |
| + | {{l_actions}} |
| + | {{l_action|act1|pro :∈ BOOL}} |
| + | {{l_end_event}} |
| + | {{l_end}} |
| | | |
− | | + | [[Category:Listing templates]] |
− | // This will add an [edit top] link at the top of all pages except preview pages
| + | ==Template== |
− | // by User:Pile0nades
| + | </noinclude><!-- |
− | | + | --><div class="typeset-l_event" >{{{1}}} ≙</div>{{comment|{{{2|not extended}}} and {{3|no convergence}}}} |
− | function editTopLink() {
| |
− | // if this is preview page or generated page, stop
| |
− | if(document.getElementById("wikiPreview") || window.location.href.indexOf("w/index.php?title=Special:") != -1) return;
| |
− | | |
− | // get the page title
| |
− | var pageTitle = document.title.split(" - ")[0].replace(" ", "_");
| |
− | | |
− | // create div and set innerHTML to link
| |
− | var divContainer = document.createElement("div");
| |
− | divContainer.innerHTML = '<div class="editsection" style="float:right;margin-left:5px;margin-top:3px;">[<a href="/w/index.php?title='+pageTitle+'&action=edit§ion=0" title="'+document.title.split(" - ")[0]+'">edit top</a>]</div>';
| |
− | | |
− | // insert divContainer into the DOM before the h1
| |
− | document.getElementById("content").insertBefore(divContainer, document.getElementsByTagName("h1")[0]);
| |
− | | |
− | }
| |
− | addOnloadHook(editTopLink);
| |
− | // addLoadEvent(editTopLink);
| |
− | | |
− | | |
− | var suiviManagerAllPages = new Array();
| |
− |
| |
− | function SuiviManagerRegexp(regexp)
| |
− | {
| |
− | var match = new RegExp(regexp);
| |
− | | |
− | for (var i=0;i<suiviManagerAllPages.length;i++) {
| |
− | var pageName = suiviManagerAllPages[i].childNodes[0].getAttribute("value");
| |
− | if (match.test(pageName)) {
| |
− | suiviManagerAllPages[i].childNodes[0].checked=true;
| |
− | }
| |
− | }
| |
− | }
| |
− |
| |
− | function SuiviManagerLiensRouges()
| |
− | {
| |
− | | |
− | for (var i=0;i<suiviManagerAllPages.length;i++) {
| |
− | var pageClass = suiviManagerAllPages[i].childNodes[1].getAttribute("class");
| |
− | if (pageClass && pageClass=="new") {
| |
− | suiviManagerAllPages[i].childNodes[0].checked=true;
| |
− | }
| |
− | }
| |
− | }
| |
− | | |
− | function SuiviManagerDeselect()
| |
− | {
| |
− | for (var i=0;i<suiviManagerAllPages.length;i++) {
| |
− | suiviManagerAllPages[i].childNodes[0].checked=false;
| |
− | }
| |
− | }
| |
− | | |
− | | |
− | function SuiviManager() {
| |
− | if (document.URL.indexOf("http://wiki.event-b.org/Special:Watchlist/edit")!=0) return;
| |
− |
| |
− | var a=0;
| |
− | var b=0;
| |
− | var interfaceMsg = new Array();
| |
− | var regexpList = new Array();
| |
− |
| |
− | //////////////////////////////////////////////////
| |
− | // Expressions régulières et liens de l'interface
| |
− | //
| |
− | // besoin d'aide pour les regexp ?
| |
− | // http://www.commentcamarche.net/javascript/jsregexp.php3
| |
− | //////////////////////////////////////////////////
| |
− | | |
− | interfaceMsg[a++] = "<b>Tout cocher</b>";
| |
− | regexpList[b++] = "^.*";
| |
− |
| |
− | interfaceMsg[a++] = "Utilisateurs";
| |
− | regexpList[b++] = "^Utilisateur:";
| |
− |
| |
− |
| |
− | interfaceMsg[a++] = "Images";
| |
− | regexpList[b++] = "^Image:";
| |
− |
| |
− | interfaceMsg[a++] = "Modèles";
| |
− | regexpList[b++] = "^Modèle:";
| |
− |
| |
− | interfaceMsg[a++] = "Aide";
| |
− | regexpList[b++] = "^Aide:";
| |
− |
| |
− | interfaceMsg[a++] = "Catégories";
| |
− | regexpList[b++] = "^Catégorie:";
| |
− |
| |
− |
| |
− | | |
− | //////////////////////////////////////////////////
| |
− | var topTag = document.getElementById("contentSub")
| |
− |
| |
− | // récupère toutes les pages
| |
− | var watchlist = document.getElementsByTagName("ul");
| |
− | | |
− | for (u=0;u<watchlist.length;u++) {
| |
− | var entries = watchlist[u].getElementsByTagName("li");
| |
− | for (i=0;i<entries.length;i++) {
| |
− | suiviManagerAllPages.push(entries[i]);
| |
− | }
| |
− | }
| |
− |
| |
− | // prépare la mini-interface
| |
− | var str = "<div style=\"background-color:#8ecfe4;font-size:1px;height:8px;border:1px solid #AAAAAA;-moz-border-radius-topright:0.5em;-moz-border-radius-topleft:0.5em;\"></div>"
| |
− | + "<div style=\"border:1px solid #6ac1de;border-top:0px solid white;padding:5px 5px 0 5px;margin-bottom:3ex;\"><p>"
| |
− | + "<div style=\"float: left; text-align: left; white-space: nowrap;\"></div>"
| |
− |
| |
− | for (var cpt = 0; cpt < interfaceMsg.length; cpt ++) {
| |
− | str += "<a href=\"javascript:SuiviManagerRegexp('" + regexpList[cpt] + "')\">"
| |
− | + interfaceMsg[cpt]
| |
− | + " ·</a> "
| |
− | }
| |
− |
| |
− | str += "<a href=\"javascript:SuiviManagerLiensRouges()\">"
| |
− | + "Retirer les liens rouges"
| |
− | + " ·</a> "
| |
− |
| |
− | str += "<a href=\"javascript:SuiviManagerDeselect()\">"
| |
− | + "<b>Enlever toutes les coches</b>"
| |
− | + " ·</a> "
| |
− |
| |
− | topTag.innerHTML = topTag.innerHTML + "<br clear=all />" + str + "<p></div>"
| |
− |
| |
− | } | |
− | | |
− | addLoadEvent(SuiviManager);
| |
− | | |
− | | |
− | /*
| |
− | * Auto Refresh
| |
− | */
| |
− | | |
− | function refresh()
| |
− | { | |
− | window.location.href = unescape(window.location);
| |
− | }
| |
− | | |
− | function refresh1min()
| |
− | { | |
− | // the timeout value should be the same as in the "refresh" meta-tag
| |
− | setTimeout( "refresh()", 60000 );
| |
− | } | |
− | | |
− | function refresh5min()
| |
− | {
| |
− | // the timeout value should be the same as in the "refresh" meta-tag
| |
− | setTimeout( "refresh()", 300000 );
| |
− | } | |
− | | |
− | if (location.href.indexOf('Special:Recentchanges') != -1) {
| |
− | addLoadEvent(refresh5min);
| |
− | } | |
− | | |
− | if (location.href.indexOf('Special:Watchlist') != -1) {
| |
− | addLoadEvent(refresh5min);
| |
− | } | |
− | | |
− | /* </nowiki></pre> */
| |