Difference between pages "User:Mathieu/monobook.js" and "Template:L event"

From Event-B
< User:Mathieu(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
m
 
imported>Mathieu
m (New page: <noinclude> ==Usage== Template use to typeset an event name in an event-b listing. ==Example== {{l_machine|AntiCollide}} {{l_refines|Safety}} {{l_sees|Network}} {{l_component|Acyclic}} {{...)
 
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}}}&nbsp;</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&section=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> */
 

Revision as of 13:42, 26 February 2009

Usage

Template use to typeset an event name in an event-b listing.

Example

MACHINE

AntiCollide

REFINES

Safety

SEES

Network

Acyclic

VARIABLES

v1

v2

INVARIANTS

inv1 :
v2 ∈ BOOL

THEOREMS

inv1 :
v2 ∈ BOOL

EVENTS

control ≙
Template:Comment

ANY

a

x

WHERE

grd1 :
x ⊆ next

WITH

y :
{{{2}}}

THEN

act1 :
pro :∈ BOOL

END

END

Template

{{{1}}} ≙

Template:Comment