miz.xsltxt

// This file is now automatically produced from the files in the MHTML directory.
// Its only reason is to have just one big .xsl file in the Mizar distro.
// So any changes should be done to the MHTML files, running 'make miz.xsl' afterwards.
// The main stylesheet mhtml_main.xsl can be used instead miz.xsl,
// provided the included .xsl files are available in the same directory

stylesheet 1.0
extension-element-prefixes = "dc";
xmlns dc "http://purl.org/dc/elements/1.1/";

output method=html;


// $Revision: 1.8 $
//
// File: mhtml_main.xsltxt - html-ization of Mizar XML, main file
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



// XSLTXT (https://xsltxt.dev.java.net/) stylesheet taking 
// XML terms, formulas and types to less verbose format.

// To produce standard XSLT from this do e.g.: 
// java -jar xsltxt.jar toXSL miz.xsltxt | sed -e 's/<!\-\- *\(<\/*xsl:document.*\) *\-\->/\1/g' >miz.xsl
// (the sed hack is there because xsl:document is not yet supported by xsltxtx)

// Then e.g.: xsltproc miz.xsl ordinal2.pre >ordinal2.pre1


// TODO: number B vars in fraenkel - done since 1.72
//       handle F and H parenthesis as K parenthesis
//       article numbering in Ref?
//       absolute definiens numbers for thesisExpansions? - done
//       do not display BlockThesis for Proof? - done, should but should be optional for Now
//       add @nr to canceled
//       Constructor should know its serial number! - needed in defs
//       possibly also article?
//       change globally 'G' to 'L' for types? -> then change the
//       hacks here and in emacs.el
//       display definiens? - done

// NOTES: constructor disambiguation is done using the absolute numbers
//        (attribute 'nr' and 'aid' of the Constructor element.
//        This info for Constructors not defined in the article is
//        taken from the .atr file (see variable $constrs)


//
// File: params.xsltxt - html-ization of Mizar XML, top-level parameters
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



// The following are user-customizable 

// mmlquery address
#mmlq= { "http://merak.pb.bialystok.pl/mmlquery/fillin.php?entry="; }
//#mmlq= {"";}

// linking methods:
// "q" - query, everything is linked to mmlquery
// "s" - self, everything is linked to these xml/html files
// "m" - mizaring and mmlquery, current article's constructs are linked to self,
//       the rest is linked to mmlquery
// "l" - local mizaring, current article's constructs are linked to self,
//       the rest to $MIZFILES/html
#linking = { "l"; }

// needed for local linking, document("") gives the sylesheet as a document
#mizfiles = { `string(/*/@mizfiles)`; }
#mizhtml  = { `concat("file://",$mizfiles,"html/")`; }

// extension for linking to other articles - either xml or html
#ext = { "html"; }

// extension for linking to other articles - either xml or html
#selfext = 
{ 
   choose 
   { 
      when [$linking = "l"] { "xml";  }
      when [$linking = "s"] { $ext;   }
      when [$linking = "m"] { "xml";  }
      when [$linking = "q"] { "html"; }
   }
}

// default target frame for links
#default_target = { if [$linking = "s"] { "_self"; } else { "mmlquery";} } 

// put titles to links or not
#titles = { "0"; }

// coloured output or not
#colored = { "0"; }


// print identifiers (like in JFM) instead of normalized names
$print_identifiers = { "1"; }

// new brackets: trying to print brackets as mizar does -
// when two or more arguments of a functor - now default
#mizar_brackets = { "1"; }

// no spaces around functor symbols
#funcs_no_spaces = { "0"; }

// print label identifiers  instead of normalized names
// this is kept separate from $print_identifiers, because
// it should be turned off for item generating
$print_lab_identifiers = { "1"; }

// print "for" in registrations - newly in version 1132
#regs_use_for = { "1"; }

// tells whether relative or absolute names are shown
#relnames= { "1"; }

// link by (now also from) inferences to ATP solutions rendered by MMLQuery; experimental - off
// 1 - static linking (to pre-generated html)
// 2 - dynamic linking to MML Query (static dli sent to MMLQuery DLI-processor)
// 3 - dynamic linking to the TPTP-processor CGI ($lbytptpcgi)
#linkby= { "0"; }

// if non zero, add icons for atp exlpanation calls to theorems and proofs in the same way as to by's
#linkarproofs= { "0"; }

// if > 0, call the mk_by_title function to create a title for by|from|;
#by_titles = { "0"; }

// If 1, the target frame for by explanations is _self
#linkbytoself = { "0"; }

// directory with by ATP solutions in HTML; each article in its own subdir
#lbydir= { "_by/"; }

// directory with by ATP solutions in DLI; each article in its own subdir
// now whole url for the CGI script
#lbydliurl= { "http://lipa.ms.mff.cuni.cz/~urban/xmlmml/html.930/_by_dli/"; }

// URL of the DLI-processor CGI
#lbydlicgi= { "http://mmlquery.mizar.org/cgi-bin/mmlquery/dli"; }

// complete prefix of the DLI-processor CGI request
$lbydlicgipref= { `concat($lbydlicgi,"?url=",$lbydliurl)`; }

// URL of the MizAR root dir
// #ltptproot= { "http://octopi.mizar.org/~mptp/"; }
#ltptproot= { "http://mws.cs.ru.nl/~mptp/"; }

// URL of the TPTP-processor CGI
#ltptpcgi= { `concat($ltptproot,"cgi-bin/")`; }

// URL of the showby CGI
#lbytptpcgi= { `concat($ltptpcgi,"showby.cgi")`; }

// URL of the showtmpfile CGI
#ltmpftptpcgi= { `concat($ltptpcgi,"showtmpfile.cgi")`; }

// tells if by action is fetched through AJAX; default is off
#ajax_by = { "0"; }


// temporary dir with  the tptp by files, needs to be passed as a param
#lbytmpdir = { ""; }

// additional params for lbytptpcgi, needs to be passed as a param
#lbycgiparams = { ""; }


// add links to tptp files for thms
#thms_tptp_links = { "0"; }

// add editing, history, and possibly other links for wiki
// the namespace for the scripts is taken from #ltptproot
#wiki_links = { "0"; }

// add buttons for editing wiki sections
#wiki_sections = { "0"; }

// domain name of the "wiki" server
#lwikihost = { "mws.cs.ru.nl"; }

// URL of the "wiki" server
#lwikiserver = { `concat("http://",$lwikihost)`; }

// URL of the "mwiki" cgi, used for mwiki actions
#lmwikicgi= { `concat($lwikiserver,"/cgi-bin/mwiki/mwiki.cgi")`; }

// name of the index page for wiki
#lmwikiindex= { "00INDEX.html"; }

// URL of the "wiki" raw cgi, showing the raw file
#lrawcgi= { `concat($lwikiserver,"/cgi-bin/mwiki/raw.cgi")`; }

// URL of the "gitweb" cgi, showing git history
#lgitwebcgi= { `concat($lwikiserver,":1234/")`; }

// name of the git repository (project) in which this page is contained -
// used for gitweb history
#lgitproject= { "mw1.git"; }

// git clone address used for wiki cloning
#lgitclone = { `concat("git://",$lwikihost,"/git/", $lgitproject)`; }

// http clone address used for wiki cloning
#lhttpclone = { `concat("http://",$lwikihost,"/git/", $lgitproject)`; }

// tells if linkage of proof elements is done; default is off
#proof_links = { "0"; }

// tells if linkage of constants is done; default is 0 (off),
// 1 tells to only create the anchors, 2 tells to also link constants
// ##TODO: 2 is implement incorrectly and should not be used now,
//         it should be done like privname (via the C key, not like now)
#const_links = { "0"; }

// tells if proofs are fetched through AJAX; default is off
// value 2 tells to produce the proofs, but not to insert the ajax calls,
// and instead insert tags for easy regexp-based post-insertion of files
// value 3 uses the ltmpftptpcgi to fetch the proof in the ajax request - like for by
#ajax_proofs = { "0"; }

// tells if ajax-able clicking requests (like proofs) are
// executed already on mouseover; default is on, but this 
// will only work of $ajax_proofs>0
#ajax_tooltips = { "1"; }

// the dir with proofs that are fetched through AJAX
#ajax_proof_dir = { "proofs"; }

// tells to display thesis after skeleton items
#display_thesis = { "1"; }

// tooltips wherever the corresponding hide/show functions apply
#hs_tooltips= { "1"; }
#hs2_tooltips= { "1"; }

// tooltips for references
#ref_tooltips= { "1"; }

// tells if only selected items are generated to subdirs; default is off
#generate_items = { "0"; }

// put ajax for references (theorems, defs, schems) to $ajax_refs_dir
// seems to be wanted in the same situations as $ajax_proofs, so it is linked to them
#mk_ajax_refs = { $ajax_proofs; }

// the dir with refs that can be fetched by AJAX
#ajax_refs_dir = { "refs"; }

// relevant only if $generate_items>0
// tells if proofs of selected items are generated to subdirs; default is off
#generate_items_proofs = { "0"; }

// add IDV links and icons
#idv =  { "0"; }

// create header info from .hdr file
#mk_header =  { "0"; }

// include comment info from .cmt file
#mk_comments =  { "0"; }

// include environ info from .evl file
#mk_environ =  { "0"; }	     

// Suppress the header and trailer of the final document. 
// Thus, you can insert the resulting document into a larger one.
#body_only = { "0"; }

$lcletters= { "abcdefghijklmnopqrstuvwxyz"; }
$ucletters= { "ABCDEFGHIJKLMNOPQRSTUVWXYZ"; } 

// name of current article (upper case)
#aname= { `string(/*/@aid)`; }

// name of current article (lower case)
#anamelc= { `translate($aname, $ucletters, $lcletters)`; }

// this needs to be set to 1 for processing MML files
#mml = { if [/Article] { "0"; } else { "1"; } }

// nr. of clusters in Typ
// this is set to 1 for processing MML files
#cluster_nr = { if [$mml = "0"] { "2"; } else { "1"; }}

// whether we print all attributes (not just those with @pid)
// this is set to 1 for processing MML files
#print_all_attrs = { $mml; }

// .atr file with imported constructors
#constrs=  { `concat($anamelc, '.atr')`; }

// .eth file with imported theorems
#thms=  { `concat($anamelc, '.eth')`; }

// .esh file with imported schemes
#schms=  { `concat($anamelc, '.esh')`; }

// .eno file with imported patterns
#patts=  { `concat($anamelc, '.eno')`; }

// .frx file with all (both imported and article's) formats
#formats=  { `concat($anamelc, '.frx')`; }

// .dcx file with vocabulary
#vocs=  { `concat($anamelc, '.dcx')`; }

// .idx file with identifier names
#ids=  { `concat($anamelc, '.idx')`; }

// .dfs file with imported definientia
#dfs=  { `concat($anamelc, '.dfs')`; }

// .hdr file with header info (done by mkxmlhdr.pl)
#hdr=  { `concat($anamelc, '.hdr')`; }

// .cmt file with comments info (done by MizComments.pl)
#cmt=  { `concat($anamelc, '.cmt')`; }

// .evl file with environ info
#evl =  { `concat($anamelc, '.evl')`; }

       
#varcolor = { "Olive"; }

#constcolor = { "Maroon"; }

#locicolor = { "Maroon"; }

#schpcolor = { "Maroon"; }

#schfcolor = { "Maroon"; }

#ppcolor = { "Maroon"; }

#pfcolor = { "Maroon"; }

#labcolor = { "Green"; }

#commentcolor = { "firebrick"; }

// use spans for brackets
#parenspans = { "1"; }

// number of parenthesis colors (see the stylesheet in the bottom)
#pcolors_nr = { "6"; }

// top level element instead of top-level document, which is hard to
// know
#top = `/`;

// debugging message
#dbgmsg = { "zzzzzzzzz"; }

// relative nr of the first expandable mode
// #first_exp = { `//Pattern[(@constrkind='M') and (@constrnr=0)][1]/@relnr`; }

// symbols, should be overloaded with different (eg tex, mathml) presentations
#for_s = { " for "; }
#ex_s = { " ex "; }
#not_s = { " not "; }
#non_s = { " non "; }
#and_s = { " & "; }
#imp_s = { " implies "; }
#equiv_s = { " iff "; }
#or_s = { " or "; }
#holds_s = { " holds "; }
#being_s = { " being "; }
#be_s = { " be "; }
#st_s = { " st "; }
#is_s = { " is "; }
#dots_s = { " ... "; }
#fraenkel_start = { " { "; }
#fraenkel_end = { " } "; }
#of_sel_s = { " of "; }
#of_typ_s = { " of "; }
#the_sel_s = { " the "; }
#choice_s = { " the "; }
#lbracket_s = { "("; }
#rbracket_s = { ")"; }
#top_proof_end = { "end;"; }




// the javascript that we are so reluctant to outsource
#mizjs1 = { 

"
function hs(obj)
{
// document.getElementById('myimage').nextSibling.style.display = 'block';
if (obj.nextSibling.style.display == 'inline')
 { obj.nextSibling.style.display = 'none'; }
else { if (obj.nextSibling.style.display == 'none')
 { obj.nextSibling.style.display = 'inline'; }
 else { obj.nextSibling.style.display = 'inline';  }}
return false;
}

function hs2(obj)
{
if (obj.nextSibling.style.display == 'block')
 { obj.nextSibling.style.display = 'none'; }
else { if (obj.nextSibling.style.display == 'none')
 { obj.nextSibling.style.display = 'block'; }
 else { obj.nextSibling.style.display = 'none';  }}
return false;
}
function hsNdiv(obj)
{
var ndiv = obj;
while (ndiv.nextSibling.nodeName != 'DIV') { ndiv = ndiv.nextSibling; }
return hs2(ndiv);
}

// remote request cache - for each url its http_request.responseText
var rrCache= {};
rrCache[0]='';

// explorer7 implements XMLHttpRequest in some strange way
// optional tooltip is passed to insertRequest
function makeRequest(obj,url,tooltip) 
{
    // if the result is cached, insert it now
    if (rrCache[url] != null)
    {
	insertRequest(obj,null,url,tooltip);
    }
    else
    {
        var http_request = false;
        if (window.XMLHttpRequest && !(window.ActiveXObject)) { // Mozilla, Safari,...
            http_request = new XMLHttpRequest();
            if (http_request.overrideMimeType) {
                http_request.overrideMimeType('text/xml');
            }
        } else if (window.ActiveXObject) { // IE
            try {
                http_request = new ActiveXObject('Msxml2.XMLHTTP');
            } catch (e) {
                try {
                    http_request = new ActiveXObject('Microsoft.XMLHTTP');
                } catch (e) {}
            }
        }
        if (!http_request) {
            alert('Giving up :( Cannot create an XMLHTTP instance');
            return false;
        }
        http_request.onreadystatechange = function() { insertRequest(obj,http_request,url,tooltip); };
        http_request.open('GET', url, true);
        http_request.send(null);
    }
}
// commented the 200 state to have local requests too
// if tooltip nonnil, obj.innerHTML is changed, and the result is put in rrCache
function insertRequest(obj,http_request,url,tooltip) 
{
    var respText = null;
    if(http_request == null) // no request done, we are called with cached result
    {
	respText = rrCache[url];
    }
    else { if (http_request.readyState == 4) { 
	respText = http_request.responseText; 
    }}

    if (respText != null) 
    {
//            if (http_request.status == 200) {
	if(http_request != null) {rrCache[url] = respText;}
	if(tooltip != null)
	{
	    obj.innerHTML = respText;	    
	}
	else
	{
	    var ndiv = obj;
	    while (ndiv.nodeName != 'SPAN') { ndiv = ndiv.nextSibling; }
	    ndiv.innerHTML = respText;
	    obj.onclick = function(){ return hs2(obj) };
	}
    }
}

// simple tooltips
var tooltip=function(){
 var id = 'tt';
 var top = 3;
 var left = 3;
 var maxw = 500;
 var speed = 10;
 var timer = 2;
 var endalpha = 95;
 var alpha = 0;
 var tt,t,c,b,h;
 var ie = document.all ? true : false;
 return{
  show:function(how,v,w){
   if(tt == null){
    tt = document.createElement('div');
    tt.setAttribute('id',id);
    document.body.appendChild(tt);
    tt.style.opacity = 0;
    tt.style.filter = 'alpha(opacity=0)';
    document.onmousemove = this.pos;
   }

   tt.style.display = 'block';
   if(how == 'url')
   {
       if(rrCache[v]==null) { 
	   tt.innerHTML ='<div>loading...</div>'; 
	   makeRequest(tt,v,1); 
       } else { 
	   tt.innerHTML = rrCache[v]; 
       }
   }
   else { if ((how == 'hs') || (how == 'hs2')) { tt.innerHTML = v.nextSibling.innerHTML; }
   else { if (how == 'txt') { tt.innerHTML = v; }
	  else { tt.innerHTML = ''; }
	}
   }

   tt.style.width = w ? w + 'px' : 'auto';
   if(!w && ie){
    tt.style.width = tt.offsetWidth;
   }
  if(tt.offsetWidth > maxw){tt.style.width = maxw + 'px'}
  h = parseInt(tt.offsetHeight) + top;
  clearInterval(tt.timer);
  tt.timer = setInterval(function(){tooltip.fade(1)},timer);
  },
  pos:function(e){
   var u = ie ? event.clientY + document.documentElement.scrollTop : e.pageY;
   var l = ie ? event.clientX + document.documentElement.scrollLeft : e.pageX;
   tt.style.top = (u - h) + 'px';
   tt.style.left = (l + left) + 'px';
  },
  fade:function(d){
   var a = alpha;
   if((a != endalpha && d == 1) || (a != 0 && d == -1)){
    var i = speed;
   if(endalpha - a < speed && d == 1){
    i = endalpha - a;
   }else if(alpha < speed && d == -1){
     i = a;
   }
   alpha = a + (i * d);
   tt.style.opacity = alpha * .01;
   tt.style.filter = 'alpha(opacity=' + alpha + ')';
  }else{
    clearInterval(tt.timer);
     if(d == -1){tt.style.display = 'none'}
  }
 },
 hide:function(){tt.style.display  = 'none';}
 };
}();

// reference show/hide - shortened because frequent, just a wrapper to tooltip.show/hide
function rs(ref) { tooltip.show('url', mizhtm + 'refs/' + ref); }
function rh() { tooltip.hide(); } 

// End -->
"; }
//
// File: keys.xsltxt - html-ization of Mizar XML, definition of keys (indexes)
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



// keys for fast constructor and reference lookup
key "M" [Constructor[@kind='M']] `@relnr` ;
key "L" [Constructor[@kind='L']] `@relnr` ;
key "V" [Constructor[@kind='V']] `@relnr` ;
key "R" [Constructor[@kind='R']] `@relnr` ;
key "K" [Constructor[@kind='K']] `@relnr` ;
key "U" [Constructor[@kind='U']] `@relnr` ;
key "G" [Constructor[@kind='G']] `@relnr` ;

key "T" [/Theorems/Theorem[@kind='T']] `concat(@articlenr,':',@nr)`;
key "D" [/Theorems/Theorem[@kind='D']] `concat(@articlenr,':',@nr)`;
key "S" [/Schemes/Scheme] `concat(@articlenr,':',@nr)`;
key "DF" [Definiens] `@relnr` ;

// patterns are slightly tricky, since a predicate pattern
// may be linked to an attribute constructor; hence the
// indexing is done according to @constrkind and not @kind
// TODO: the attribute<->predicate change should propagate to usage
//       of "is"
// Expandable modes have all @constrkind='M' and @constrnr=0,
// they are indexed separately only on their @relnr (@pid)
key "P_M" [Pattern[(@constrkind='M') and (@constrnr>0)]] `@constrnr` ;
key "P_L" [Pattern[@constrkind='L']] `@constrnr` ;
key "P_V" [Pattern[@constrkind='V']] `@constrnr` ;
key "P_R" [Pattern[@constrkind='R']] `@constrnr` ;
key "P_K" [Pattern[@constrkind='K']] `@constrnr` ;
key "P_U" [Pattern[@constrkind='U']] `@constrnr` ;
key "P_G" [Pattern[@constrkind='G']] `@constrnr` ;
key "EXP" [Pattern[(@constrkind='M') and (@constrnr=0)]] `@relnr` ;

key "F" [Format] `@nr`;

key "D_G" [Symbol[@kind='G']] `@nr`;
key "D_K" [Symbol[@kind='K']] `@nr`;
key "D_J" [Symbol[@kind='J']] `@nr`;
key "D_L" [Symbol[@kind='L']] `@nr`;
key "D_M" [Symbol[@kind='M']] `@nr`;
key "D_O" [Symbol[@kind='O']] `@nr`;
key "D_R" [Symbol[@kind='R']] `@nr`;
key "D_U" [Symbol[@kind='U']] `@nr`;
key "D_V" [Symbol[@kind='V']] `@nr`;

// identifiers
key "D_I" [Symbol[@kind='I']] `@nr`;

// keys for absolute linkage inside proofs; 
// requires preprocessing by addabsrefs, otherwise wrong results,
// so commented now (could be uncommented using conditional include probably)

// lookup for local constants
key "C" [Let|Given|TakeAsVar|Consider|Set|Reconsider] `@plevel` ;

// lookup for propositions
key "E" [Proposition|IterEquality|Now] `concat(@nr,":",@plevel)` ;

// lookup for scheme functors and predicates
key "f" [SchemeFuncDecl] `concat(@nr,":",@plevel)` ;
key "p" [SchemePredDecl] `concat(@nr,":",@plevel)` ;

// lookup for private functors and predicates
key "pf" [DefFunc] `concat(@nr,":",@plevel)` ;
key "pp" [DefPred] `concat(@nr,":",@plevel)` ;

// lookup for comments
key "CMT" [Comment] `@endline`;
//
// File: print_simple.xsltxt - html-ization of Mizar XML, simple printing funcs
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



// pretty print variables and labels

// ##TODO: link variables and consts to their introduction?


// private - look up the name of id
tpl get_vid_name(#vid)
{
  for-each [document($ids, /)] 
  { 
     for-each [key('D_I', $vid)] { `@name`; }
  }
}

tpl pqvar(#nr, #vid) 
{ 
    if [($print_identifiers > 0) and ($vid > 0)] 
    {
       $nm = { get_vid_name(#vid = $vid); }

       if [$colored = "1"] 
       { 
	  <font 
	  { 
	     @color = $varcolor; 
	     if [$titles="1"] { @title=`concat("b",$nr)`; } 
	     $nm; 
          }
       }
       else 
       { 
          $nm;
       }
    }
    else 
    { 
       pvar(#nr = $nr); 
    }
}


tpl pvar(#nr) { if [$colored="1"] { <font { @color=$varcolor; 
    "b"; <sub { $nr;} } } else { "b"; <sub { $nr;} } }

tpl pconst(#nr) {  if [$colored="1"] { <font { @color=$constcolor; 
    "c"; <sub { $nr;} } } else { "c"; <sub { $nr;} } }

// #pl gives the optional proof level
tpl ppconst(#nr, #vid, #pl) 
{ 
    if [($print_identifiers > 0) and ($vid > 0)] 
    {
       $ctarget = 
       { 
         if [($const_links>0) and  ($pl)] { "c"; $nr; addp(#pl=$pl); } 
	 else { `concat("c",$nr)`; }
       }

       $nm = { get_vid_name(#vid = $vid); }

       if [($const_links=2)] // const_links imply colored here
       {
	  <a 
	  { 
	      @class = "txt"; 
	      @href  = `concat("#",$ctarget)`;
	      <font 
	      { 
	         @color = $constcolor; 
		 if [$titles="1"] { @title = $ctarget; } 
		 $nm; 
	      } 
          } 
       }       
       else { if [$colored = "1"] 
       { 
	  <font 
	  { 
	     @color = $constcolor; 
	     if [$titles="1"] { @title = $ctarget; } 
	     $nm; 
          } 
       }
       else { $nm;} } 
    }
    else { pconst(#nr = $nr); }
}

tpl pploci(#nr) 
{ 
    if [($print_identifiers > 0) and ($proof_links>0)]
    {
      $pl = get_nearest_level(#el = `..`); 
      absconst(#nr = `@nr`, #pl = $pl);
    }
    else 
    { 
       pconst(#nr=`@nr`); 
    }
}

tpl ploci(#nr) {  if [$colored="1"] { <font { @color=$locicolor; 
    "a"; <sub { $nr;} } } else { "a"; <sub { $nr;} } }

tpl pschpvar(#nr) {  if [$colored="1"] { <font { @color=$schpcolor; 
    "P"; <sub { $nr;} } } else { "P"; <sub { $nr;} } }

tpl pschfvar(#nr) {  if [$colored="1"] { <font { @color=$schfcolor; 
    "F"; <sub { $nr;} } } else { "F"; <sub { $nr;} } }

tpl pppred(#nr) {  if [$colored="1"] { <font { @color=$ppcolor; 
    "S"; <sub { $nr;} } } else { "S"; <sub { $nr;} } }

tpl ppfunc(#nr) {  if [$colored="1"] { <font { @color=$pfcolor; 
    "H"; <sub { $nr;} } } else { "H"; <sub { $nr;} } }


tpl pplab(#nr, #vid, #txt)
{ 
    if [($print_lab_identifiers > 0) and ($vid > 0)]
    {

       $nm = { get_vid_name(#vid = $vid); }

       <span 
       {
          @class="lab";
          if [$colored = "1"] 
	  { 
	     <font 
	     { 
	        @color = $labcolor; 
	        if [$titles="1"] { @title=`concat("E",$nr)`; } 
	        $nm; 
             } 
          }
	  else { $nm;}
       }
    }
    else 
    {
       if [$txt]  
       { 
          plab1(#nr = $nr, #txt = $txt); 
       } 
       else { plab(#nr = $nr); }
    }
}

tpl plab(#nr) 
{ 
   <span
   {  
      @class="lab";
      if [$colored="1"] { <font { @color=$labcolor; "E"; $nr;} }  
      else { "E"; $nr;} 
   } 
}

tpl plab1(#nr,#txt) 
{ 
   <span
   {  
      @class="lab";
      if [$colored="1"] { <font { @color=$labcolor; $txt; $nr;} }  
      else { $txt; $nr;} 
   } 
}

tpl pkeyword(#str) { <span { @class = "kw"; $str; } }

tpl pcomment0(#str) { <span { @class="comment"; if [$colored="1"] {
<font {@color=$commentcolor; ":: "; $str;}} else { ":: "; $str;}}}

tpl pcomment(#str) { pcomment0(#str=$str); <br;}

// this assumes comments with :: already
tpl pcommentedblock(#str) 
{ 
   <div { @class="comment mathjax"; 
     if [$colored="1"] {
        <font {@color=$commentcolor; br(#text=$str);}
     }
     else {  br(#text=$str); }
   }
}

// argument list
tpl arglist(#separ,#elems) 
{ 
   for-each [$elems] 
   {
      ploci(#nr = `position()`); 
      if [not(position() = last())] { $separ; } 
   }
}

// translate newlines to <br;
tpl br(#text) {
  choose {
    when [contains($text,'&#xa;')] {
      `substring-before($text,'&#xa;')`;
      <br;
       br(#text = `substring-after($text,'&#xa;')`);
    }
    otherwise { $text; }
  }
}



// like jlist, but with loci
tpl alist(#j, #sep1, #sep2, #elems) 
{ 
   for-each [$elems] 
   {
      apply[.]; 
      if [not(position() = last())] 
      {  
         $sep1; 
	 ploci(#nr = `$j+position()`); 
	 $sep2; 
      } 
   }
}

//
// File: utils.xsltxt - html-ization of Mizar XML, various utility functions
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)


#pid_Ex 		= { "-1"; } // usually NegFrmPtr
#pid_Ex_Univ 		= { "-2"; } // usually UnivFrmPtr
#pid_Ex_InnerNot 	= { "-3"; } // usually NegFrmPtr
#pid_Impl 		= { "-4"; } // usually NegFrmPtr
#pid_Impl_And 		= { "-5"; } // usually ConjFrmPtr       
#pid_Impl_RightNot 	= { "-6"; } // usually NegFrmPtr
#pid_Iff 		= { "-7"; } // usually ConjFrmPtr
#pid_Or 		= { "-8"; } // usually NegFrmPtr
#pid_Or_And 		= { "-9"; } // usually ConjFrmPtr
#pid_Or_LeftNot 	= { "-10"; } // usually NegFrmPtr
#pid_Or_RightNot 	= { "-11"; } // usually NegFrmPtr

// means that "not" will not be used
tpl is_positive(#el) { for-each [$el] {
    if [(name()="Not")] { 
       if [Pred[(@kind='V') or (@kind='R')]] { 
	  $pi = { patt_info(#k=`*[1]/@kind`, #nr=`*[1]/@nr`, #pid =`*[1]/@pid`); }
	  $antonym = cadr(#l=$pi);
	  `$antonym mod 2`; }
       else { "0"; }
    }
    else { 
	 if [(name()="Pred") and ((@kind='V') or (@kind='R'))] {
	    $pi = { patt_info(#k=`@kind`, #nr=`@nr`, #pid =`@pid`); }
	    $antonym = cadr(#l=$pi);
	    `($antonym + 1) mod 2`;
	 }
	 else { "1"; }}}}

tpl is_negative(#el) { $pos = { is_positive(#el=$el); } `1 - $pos`;}

tpl count_positive(#els,#nr) {  
    if [$nr > 0] {
       $el1=`$els[position()=$nr]`;
       $res1 = { is_positive(#el=`$els[position()=$nr]`); }
       $res2 = { count_positive(#els=$els,#nr=`$nr - 1`); }
//DEBUG       `concat($res1,":",$res2)`;
       `$res1 + $res2`;
    }
    else { "0"; }}

// if $neg, then put negative, striping the negation
tpl put_positive(#separ,#els,#nr,#neg,#i) { if [$nr > 0] {
    $el1=`$els[position()=1]`;
    $pos = is_positive(#el=$el1);
    $pos1 = { if [$neg="1"] { `($neg + $pos) mod 2`; } else { $pos; }}
    if [$pos1="1"] { 
       $nm = `name($el1)`;
       if [$neg="1"] { // change this if is_positive changes!
	  choose {
	  when [$nm="Not"]  { apply[$el1/*[1]](#i=$i); }
	  when [$nm="Pred"]  { apply[$el1](#i=$i,#not="1"); }
	  otherwise { $dbgmsg; $nm; } }
       }
       else { if [$nm="Not"]  { apply[$el1/*[1]](#i=$i,#not="1"); }
	      else { apply[$el1](#i=$i); }} 
       if [$nr > 1] { $separ; } }
    put_positive(#separ=$separ,#els=`$els[position() > 1]`,#nr=`$nr - $pos1`,#neg=$neg); } }

tpl is_or(#el) { for-each [$el] { if [(@pid=$pid_Or) 
        and (*[1][@pid=$pid_Or_And]) and (count(*[1]/*)=2)
	and (*[1]/*[1][@pid=$pid_Or_LeftNot])
	and (*[1]/*[2][@pid=$pid_Or_RightNot])]
 { "1"; } else { "0"; }}}

// now also used when included "or" ate the implicant
tpl is_or1(#el) { for-each [$el] { if [((@pid=$pid_Or) or (@pid=$pid_Impl)) 
        and (*[1][@pid=$pid_Or_And]) and (count(*[1]/*)>=2)]
    { "1"; } else { "0"; }}}


// used when is_or failed
tpl is_or3(#el) { for-each [$el] { if [(@pid=$pid_Or) 
        and (*[1][@pid=$pid_Or_And]) and (count(*[1]/*)=2)]
	{ $neg1 = { is_negative(#el=`*[1]/*[1]`); }
          $neg2 = { is_negative(#el=`*[1]/*[2]`); }
	  `$neg1 * $neg2`; }
    else { "0"; }}}

// used when is_or3 failed
tpl is_or4(#el) { for-each [$el] { if [(@pid=$pid_Or) 
        and (*[1][@pid=$pid_Or_And]) and (count(*[1]/*)=2)]
    { "1"; } else { "0"; }}}

tpl is_impl(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)=2)
	and (*[1]/*[2][@pid=$pid_Impl_RightNot])]
 { "1"; } else { "0"; }}}


tpl is_impl1(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)>=2)] {
	choose {
	when [*[1]/*[@pid=$pid_Impl_RightNot]] { "2"; }
	when [name(*[1]/*[position()=last()]) = "For"] { "4"; }
	otherwise {
	  $neg1 = { is_negative(#el=`*[1]/*[position()=last()]`); }
	  if [$neg1 = "1"] { "3"; }
	  else { "5"; } }
        } } else { "0"; }}}
	  

tpl is_impl2(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)>=2)
	and ((*[1]/*[@pid=$pid_Impl_RightNot]))]
 { "1"; } else { "0"; }}}

// used when is_impl2 failed
tpl is_impl3(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)>=2)]
	{ is_negative(#el=`*[1]/*[position()=last()]`); }
	else { "0"; }}}

// used when is_impl3 failed
tpl is_impl4(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)>=2)
	and (name(*[1]/*[position()=last()]) = "For")]
	{ "1"; } else { "0"; }}}

// used when is_impl4 failed
tpl is_impl5(#el) { for-each [$el] { if [(@pid=$pid_Impl) 
        and (*[1][@pid=$pid_Impl_And]) and (count(*[1]/*)>=2)]
	{ "1"; } else { "0"; }}}



tpl is_equiv(#el) { for-each [$el] {
       $e1 = { if [(@pid=$pid_Iff) and (count(*)=2)] {
		  $i1 = { is_impl(#el=`$el/*[1]`); } 
		  if [$i1="1"] { is_impl(#el=`*[2]`); }
		  else { "0"; }}
	       else { "0"; } }
       if [$e1="1"] { 
	  $res1 = { are_equal( #el1=`*[1]/*[1]/*[1]`, 
			       #el2=`*[2]/*[1]/*[2]/*[1]`); }
	  $res2 = { are_equal( #el1=`*[2]/*[1]/*[1]`, 
			       #el2=`*[1]/*[1]/*[2]/*[1]`); }
	  if [($res1="1") and ($res2="1")] { "1"; }
          else { "0"; }}
       else  { $e1; }}}

//  recursive equality on subnodes and attributes
tpl are_equal(#el1,#el2) { 
    if[ not(name($el1)=name($el2)) or not(count($el1/*)=count($el2/*))
	or not(count($el1/@*)=count($el2/@*))] { "0"; }
    else { 
	 $s1 = { for-each [$el1/@*] { `string()`;} }
	 $s2 = { for-each [$el2/@*] { `string()`;} }
	 if [not($s1=$s2)] { "0"; }
    else 
     { are_equal_many(#els1=`$el1/*`,#els2=`$el2/*`,#nr=`count($el1/*)`); }}}

tpl are_equal_many(#els1,#els2,#nr) { if [$nr > 0] {
    $el1=`$els1[position()=$nr]`;
    $el2=`$els2[position()=$nr]`; 
    $res1 = { are_equal(#el1=$el1, #el2=$el2); }
    if [$res1="1"] { are_equal_many(#els1=$els1, #els2=$els2, #nr=`$nr - 1`);}
    else { "0"; }} else { "1"; }}

//  recursive equality on subnodes and attributes upto the @vid attribute
tpl are_equal_vid(#el1,#el2) { 
    if[ not(name($el1)=name($el2)) or not(count($el1/*)=count($el2/*))
	or not(count($el1/@*)=count($el2/@*))] { "0"; }
    else { 
	 $s1 = { for-each [$el1/@*] { if[not(name()="vid")] { `string()`;}} }
	 $s2 = { for-each [$el2/@*] { if[not(name()="vid")] { `string()`;}} }
	 if [not($s1=$s2)] { "0"; }
    else 
     { are_equal_many_vid(#els1=`$el1/*`,#els2=`$el2/*`,#nr=`count($el1/*)`); }}}

tpl are_equal_many_vid(#els1,#els2,#nr) { if [$nr > 0] {
    $el1=`$els1[position()=$nr]`;
    $el2=`$els2[position()=$nr]`; 
    $res1 = { are_equal_vid(#el1=$el1, #el2=$el2); }
    if [$res1="1"] { are_equal_many_vid(#els1=$els1, #els2=$els2, #nr=`$nr - 1`);}
    else { "0"; }} else { "1"; }}





tpl lc(#s) { `translate($s, $ucletters, $lcletters)`; }
tpl uc(#s) { `translate($s, $lcletters, $ucletters)`; }


// utilities for adding lemma names
tpl addp(#pl) { if [string-length($pl)>0] { ":"; $pl; }}
tpl propname(#n,#pl) { "E"; $n; addp(#pl=$pl); }

// poor man's data structure, aka "colon-list"
#nil = { ""; }
tpl cons(#h,#t) { `concat($h,":",$t)`; }
tpl car(#l) { `substring-before($l,":")`;}
tpl cdr(#l) { `substring-after($l,":")`;}
tpl cadr(#l) { car(#l=cdr(#l=$l));}
tpl cddr(#l) { cdr(#l=cdr(#l=$l));}
tpl third(#l) { car(#l=cddr(#l=$l)); }
tpl cdddr(#l) { cdr(#l=cddr(#l=$l));}


// poor man's 0-based integer arrays (integer is non-negative and four digits long now)
// the biggest identifier number is 1061 for jordan7 in MML 758
#int_size = { "4"; }


// #index must be 0-based
tpl arr_ref(#array,#index) 
{ 
  $beg     = `$int_size * $index`;

  `number(substring($array, $beg, $beg + $int_size))`;
}


tpl apush(#array,#obj) 
{
   $obj1 = { arr_pad_obj(#obj); }

   `concat($array, $obj1)`;
}


tpl arr_set(#array,#index,#obj) 
{ 
  $obj1    = { arr_pad_obj(#obj); }
  $beg     = `$int_size * $index`;
  $end     = `$beg + $int_size`;
  $prefix  = `substring($array, 0, $beg)`;
  $postfix = `substring($array, $end)`;

  `concat($prefix, $obj1, $postfix)`;
}

// explicit for speed
tpl arr_zeros(#l) 
{
  choose 
  { 
      when [$l = 0] { "";}
      when [$l = 1] { "0";}
      when [$l = 2] { "00";}
      when [$l = 3] { "000";}
      when [$l = 4] { "0000";}
      when [$l = 5] { "00000";}
  }
}


tpl arr_pad_obj(#obj)
{
   $length  = `$int_size - string-length($obj)`;
   $padding = { arr_zeros(#l = $length); }

   `concat($padding, $obj)`; 
}


// List utilities

tpl list(#separ,#elems) { 
 for-each [$elems] {
  apply[.]; if [not(position()=last())] { copy-of $separ; } }
}

// List utility with additional arg - now only used for formula lists
tpl ilist(#separ,#elems,#i,#pr) { 
 for-each [$elems] {
  apply[.](#i=$i,#pr=$pr); if [not(position()=last())] { copy-of $separ; } }
}

// newlined list
tpl nlist(#separ,#elems) { 
 for-each [$elems] {
  apply[.]; if [not(position()=last())] { <br; copy-of $separ; } }
}

// newlined andlist
tpl andlist(#elems) { 
 for-each [$elems] {
  apply[.]; if [not(position()=last())] { pkeyword(#str="and "); <br; } }
}


tpl dlist(#separ,#elems) { 
 for-each [$elems] {
  <div { apply[.]; if [not(position()=last())] { copy-of $separ; } } }
}


// Pretty print constants with their types.
// This now assumes that all #elems are Typ.
// For subseries of consts with the same Typ, 
// the Typ is printed only once.
// #sep2 is now either "be " or "being ", 
// comma is added automatically.
// #pl passes proolevel if after addabsrefs processing 
// (needed for const_links)
tpl jtlist(#j,#sep2,#elems,#pl) 
{ 
   $addpl = { if [$const_links>0] { addp(#pl = $pl); } }

   for-each [$elems] 
   { 
      $nr1 = `$j+position()`;
      if [$const_links>0] { <a { @NAME=`concat("c",$nr1,$addpl)`; } }

      ppconst(#nr = $nr1, #vid = `@vid`);

      if [position()=last()] 
      { 
         $sep2; apply[.]; 
      }
      else 
      { 
         $eq1 = { are_equal_vid(#el1=`.`,#el2=`following-sibling::*[1]`); }

	 if [$eq1="0"] { $sep2; apply[.]; } 

	 ", "; 
      }
   } 
}


// translate constructor (notation) kinds to their mizar/mmlquery names
tpl mkind(#kind) 
{
   choose 
   { 
      when [$kind = 'M'] { "mode";}
      when [$kind = 'V'] { "attr";}
      when [$kind = 'R'] { "pred";}
      when [$kind = 'K'] { "func";}
      when [$kind = 'G'] { "aggr";}
      when [$kind = 'L'] { "struct";}
      when [$kind = 'U'] { "sel";}
   }
}

// translate reference kinds to their mizar/mmlquery names
tpl refkind(#kind) 
{
  choose 
  { 
      when [$kind = 'T'] { "th";}
      when [$kind = 'D'] { "def";}
      when [$kind = 'S'] { "sch";}
  }
}


// return first symbol corresponding to a constructor ($,$nr);
// sometimes we know the $pid or even the formatnr ($fnr) precisely;
// if nothing found, just concat #k and #nr; #r says to look for
// right bracket instead of left or fail if the format is not bracket
tpl abs1(#k, #nr, #r, #fnr, #pid) 
{
//DEBUG    "abs1:"; $k; ":"; $fnr; ":";
  $fnr1 = { if [$fnr] { $fnr;} else { formt_nr(#k=$k,#nr=$nr,#pid=$pid);} }

  for-each [document($formats,/)] 
  {
     if [not(key('F',$fnr1))] 
     { 
        `concat($k,$nr)`; 
     }
     else 
     {
        for-each [key('F',$fnr1)] 
	{
          $snr  = `@symbolnr`; 
	  $sk1  = `@kind`; 
	  $sk   = { if [$sk1="L"] { "G";} else { $sk1; } }
	  $dkey = `concat('D_',$sk)`;
          $rsnr = { if [$sk='K'] { `@rightsymbolnr`; } } 

	  // return nothing if right bracket of nonbracket symbol is asked
	  // shouldn't it be an error?
	  if [not($r='1') or ($sk='K')] 
	  {
	     for-each [document($vocs,/)] 
	     {
	        if [key($dkey,$snr)] 
		{
		   for-each [key($dkey,$snr)[1]] 
		   { 
		      if [($sk='K') and ($r='1')] 
		      { 
		         for-each [key('D_L',$rsnr)[1]] { `@name`; } 
		      }
		      else 
		      {  
		         `@name`; 
		      }
                   } 
                } 
		// try the built-in symbols
		else 
		{ 
		   choose 
		   { 
		      when [($snr='1') and ($sk='M')] { "set"; }
		      when [($snr='1') and ($sk='R')] { "="; }
		      when [($snr='1') and ($sk='K')] 
		      { 
		         if [$r='1'] { "]"; } else { "["; } 
                      } 
		      when [($snr='2') and ($sk='K')] 
		      { 
		         if [$r='1'] { "}"; } else { "{"; } 
		      }
		      otherwise { `concat($k,$nr)`; } 
		   } 
		} 
	     } 
	  } 
        } 
     } 
  } 
}

// private for abs1
tpl formt_nr(#k, #nr, #pid) 
{ 
   car(#l = patt_info(#k = $k, #nr = $nr, #pid = $pid));
}


// private for patt_info
tpl mk_vis_list(#els) 
{ 
   for-each [$els] { `@x`; ":"; }
}

// private for patt_info - 
// assumes we already are inside the right pattern
tpl encode_std_pattern(#k)
{
   $shift0 = { if [@antonymic] {"1";} else {"0";}}
   $shift  = { if [($k="V") and (@kind="R")] { `2 + $shift0`; } 
               else { $shift0; } 
             }
   $plink  = { if [@redefnr>0] { "1"; } else { "0"; } }
   $vis    = mk_vis_list(#els=`Visible/Int`); 
   cons(#h = `@formatnr`,
        #t = cons(#h = $shift, #t = cons(#h = $plink, #t = $vis)));
}

// this is a small hack to minimize chasing patterns
// returns list [formatnr, antonymic or expandable (+2 if attrpred),
//               redefinition | visiblelist]
tpl patt_info(#k, #nr, #pid) 
{
   $k1     = { if [$k="L"] { "G"; } else { $k; } }
   $typ    = `($k1 = "G") or ($k1="M")`;
   $pkey   = `concat('P_',$k1)`;

   if [$pid>0] 
   {
      $doc = { if [($typ and key('EXP',$pid)) 
		     or (key($pkey,$nr)[$pid=@relnr])]  { ""; } else { $patts; }
             }

      for-each [document($doc,/)] 
      {
	   if [$typ and key('EXP',$pid)] 
	   { 
	      for-each [key('EXP',$pid)] 
	      { 
	         $vis = mk_vis_list(#els = `Visible/Int`);
		 cons(#h = `@formatnr`, 
		      #t = cons(#h ="1",#t = cons(#h = "0",#t = $vis)));
	      } 
	   }
	   else 
	   { 
	      if [key($pkey,$nr)[$pid=@relnr]] 
	      {
	         for-each [key($pkey,$nr)[$pid=@relnr]] 
		 {
		    encode_std_pattern(#k = $k);
              } 
	   }
	      else 
	      { 
	         "failedpid:"; $k1;":";$nr;":"; $pid;":";
	      }
           }
       }
   }
   else 
   { 
      $doc = { if [key($pkey,$nr)] { ""; } else { $patts; } }

      for-each [document($doc,/)] 
      {
         for-each [key($pkey,$nr)[position()=1]] 
	 {
	    encode_std_pattern(#k = $k);
	 }
      }
   }
}


// the string length #ls does not change;
// test if the #n-th position in #pl from back is underscore,
// if so, cut it and what follows it,
// otherwise try with n+1
// called externally with #n=1;
// $n<10 is probably needed to guard the recursion - limits us
// to nine digit numbers of previous blocks - seems safe now
tpl get_parent_level(#pl, #ls, #n) 
{
    $p  = { `$ls - $n`; }     
    $p1 = { `$ls - ($n + 1)`; }

    if [substring($pl, $p, 1) = '_']
    { 
       `substring($pl, 1, $p1)`; 
    }
    else 
    { 
       if [$n < 10] { get_parent_level(#pl = $pl, #ls = $ls, #n = `$n+1`); }
    } 
}



tpl add_hs_attrs 
{ 
  @class="txt"; 
  if [$hs_tooltips="1"]
  { 
     @onmouseover="tooltip.show('hs',this)"; 
     @onmouseout="tooltip.hide()"; 
  }
  @onclick="hs(this)"; 
  @href="javascript:()"; 
}

tpl add_hs2_attrs 
{
  @class="txt"; 
  if [$hs2_tooltips="1"]
  { 
     @onmouseover="tooltip.show('hs2',this)"; 
     @onmouseout="tooltip.hide()"; 
  }
  @onclick="hs2(this)"; 
  @href="javascript:()"; 
}

tpl add_hsNdiv_attrs { @class="txt"; @onclick="hsNdiv(this)"; @href="javascript:()"; }

tpl add_ajax_attrs(#u) 
{ 
  @class="txt"; 
  if [$ajax_tooltips="1"]
  { 
     @onmouseover=`concat("tooltip.show('url','", $u, "')")`; 
     @onmouseout="tooltip.hide()"; 
  }
  @onclick=`concat("makeRequest(this,'",$u,"')")`;
  @href="javascript:()"; 
}
//
// File: frmtrm.xsltxt - html-ization of Mizar XML, code for terms, formulas, and types
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



// Formulas

// #i is nr of the bound variable, 0 by default 
// #k is start of the sequence of vars with the same type, $i by default 
// we now output only one typing for such sequences
// #ex tells that we should print it as existential statement,
// i.e. also omitting the first descending Not (the caller 
// should guarantee that there _is_ a Not after the block of For-s)
// #pr tells to put the formula in paranthesis
tpl [For](#i,#k,#ex,#pr) { 
  $j = { if [$i] { $i;} else { "0"; } }
  $l = { if [$k] { $k;} else { $j; } }

  if [$l = $j] { // print initial quantifier if at the beginning of var segment
     if [$pr] { copy-of $lbracket_s; " "; }
     if [$ex="1"] { copy-of $ex_s; } else { copy-of $for_s; }
  }
  pqvar(#nr = `$j + 1`, #vid = `@vid`);

  $nm = { `name(*[2])`; }
  $eq1 = { if [($nm = "For") and (*[1]/@nr = *[2]/*[1]/@nr)]
	      { are_equal(#el1=`*[1]`,#el2=`*[2]/*[1]`); }
           else { "0"; } }

  if [$eq1="1"]  {  ", "; apply[*[2]](#i=`$j+1`,#k=$l,#ex=$ex,#pr=$pr); }
  else {
  if [$ex="1"] { 
  copy-of $being_s; apply[*[1]](#i=`$j + 1`); 
  if [$nm = "For"] { apply[*[2]](#i=`$j+1`,#ex=$ex); }
  else { copy-of $st_s; // $nm;
   if [($nm = "And") or (name(Not/*[1]) = "And") or (name(Not/*[1]) = "For")] { <br; }
   apply[Not/*[1]](#i=`$j+1`); 
   if [Pred|PrivPred|Is|Verum|ErrorFrm] { // " PREDFOR "; 
      apply[*[2]](#i=`$j+1`,#not="1"); } // for antonymous Preds
   else { if [And] { copy-of $lbracket_s; " "; 
        if [And[@pid=$pid_Or_And]]
	{
		 for-each [*[2]/*] { if [position()>1] { copy-of $or_s; }
		   $neg1 = { is_negative(#el=`.`); }
		   if [$neg1 = "1"] {
		   if [name() = "Not"] { apply[*[1]](#i=`$j+1`); } 
		     // now Pred, which is antonymous
		     else { apply[.](#i=`$j+1`,#not="1"); } }
                   else { if [name() = "For"] { apply[.](#i=`$j+1`,#ex="1"); } 
		   else { " not "; apply[.](#i=`$j+1`); } } }
	      }
       else { // pretend this is an impl
	ilist(#separ = $and_s, #elems=`*[2]/*[position()<last()]`, #i=`$j+1`,#pr="1"); copy-of $imp_s; 
	choose {
	when [*[2]/*[@pid=$pid_Impl_RightNot]] {  apply[*[2]/*[@pid=$pid_Impl_RightNot]/*[1]](#i=`$j+1`); }
	when [name(*[2]/*[position()=last()]) = "For"] { apply[*[2]/*[position()=last()]](#i=`$j+1`,#ex="1"); }
	otherwise {
	  $neg1 = { is_negative(#el=`*[2]/*[position()=last()]`); }
	  if [$neg1 = "1"] { if [name(*[2]/*[position()=last()]) = "Not"] {
			apply[*[2]/*[position()=last()]/*[1]](#i=`$j+1`); } 
			// now Pred, which is antonymous
                     else { apply[*[2]/*[position()=last()]](#i=`$j+1`,#not="1"); } }
	  else { copy-of $not_s; apply[*[2]/*[position()=last()]](#i=`$j+1`); } }
        }}  " "; copy-of $rbracket_s; }
    }
  }}
  else { 
   copy-of $being_s; apply[*[1]](#i=`$j + 1`); if [not(($nm = "For") or ($nm="Not"))] {copy-of $holds_s;} 
   if [($nm = "And") or ($nm="For")] { <br; }
   if [$nm="Not"] {  " ";  apply[*[2]](#i=`$j+1`,#st="1"); }
   else { " "; apply[*[2]](#i=`$j+1`); }}
  if [$pr] { " "; copy-of $rbracket_s; }
 } }

// tpl [And/For] { <div {"for B being"; apply[*[1]]; 	
//                copy-of $holds_s; <div { @class="add";  apply[*[2]]; } } }


// return 1 if this is a Not-ended sequence of For-s
tpl check_for_not(#el) { 
    if [(name($el)="Not") or (name($el)="Pred")] { is_negative(#el=$el); } 
    else { if [(name($el)="And") and (($el/@pid = $pid_Or_And) or ($el/@pid = $pid_Impl_And))] { "1"; }
    else { if [name($el)="For"] { check_for_not(#el=`$el/*[2]`); }
    else { "0"; }}}}

tpl [Not](#i,#pr,#st) 
{ 
    $fnb = { if [For] { check_for_not(#el=`*[1]/*[2]`); } else { "0"; } }
    if [$fnb="1"]  { apply[*[1]](#i=$i,#ex="1"); }
    else { if [Pred|Is|PrivPred|Verum|ErrorFrm] {  if [$st="1"] { copy-of $holds_s; }
	   apply[*[1]](#i=$i,#not="1"); }
    else 
    { 
         $i3= is_impl1(#el=`.`);
	 if [$i3 > 0] { // " IMPL1 "; $i3; 
            if [$st="1"] { copy-of $st_s; } else { copy-of $lbracket_s; " "; }
	     if [$i3=2] {
		ilist(#separ = $and_s, #elems=`*[1]/*[not(@pid=$pid_Impl_RightNot)]`, #i=$i,#pr="1"); 
		if [$st="1"] { copy-of $holds_s; <br; } else { copy-of $imp_s; }
		apply[*[1]/*[@pid=$pid_Impl_RightNot]/*[1]](#i=$i); }
             else { 
	        ilist(#separ = $and_s, #elems=`*[1]/*[position()<last()]`, #i=$i,#pr="1"); if [$st="1"] { copy-of $holds_s; <br; } else { copy-of $imp_s; }
                choose {
		when [$i3=3] { 
		     if [name(*[1]/*[position()=last()]) = "Not"] {
			apply[*[1]/*[position()=last()]/*[1]](#i=$i); } 
			// now Pred, which is antonymous
                     else { apply[*[1]/*[position()=last()]](#i=$i,#not="1"); } }
		when [$i3=4] { 
		     apply[*[1]/*[position()=last()]](#i=$i,#ex="1"); }
		when [$i3=5] { 
		     copy-of $not_s; apply[*[1]/*[position()=last()]](#i=$i); }
                }} if [not($st="1")] { " "; copy-of $rbracket_s; }

         }
         else {
	      if [$st="1"] { copy-of $holds_s; <br; }
	      $i1_1= is_or1(#el=`.`);
	      $i1= { if[$i1_1="1"] { "1"; } else {  // artifficially system-constructed complex fla, try some reconstruction
		     if[not(@pid) and (name(*[1])="And") and (count(*[1]/*)>=2)] { "1"; } else { "0";}}}
	      if [$i1="1"] { copy-of $lbracket_s; " "; // " OR1 "; 
		 for-each [*[1]/*] { if [position()>1] { copy-of $or_s; }
		   $neg1 = { is_negative(#el=`.`); }
		   if [$neg1 = "1"] {
		   if [name() = "Not"] { apply[*[1]](#i=$i); } 
		     // now Pred, which is antonymous
		     else { apply[.](#i=$i,#not="1"); } }
                   else { if [name() = "For"] { apply[.](#i=$i,#ex="1"); } 
		   else { copy-of $not_s; apply[.](#i=$i); } } }  " "; copy-of $rbracket_s;
	      }

              else { copy-of $not_s; if[@pid] { comment { "HUMANRECFAILED"; } } // else {"NOPID  ";} 
                     apply[*[1]](#i=$i); } } } } 
} 
// this was too AI, mizar is much simpler
// 	     $cnt=`count(*[1]/*)`; 
// 	     $pcnt1 = { if [$i3="1"] { count_positive(#els=`*[1]/*`,#nr=$cnt); } else {"10000";} }
// 	     $pcnt = $pcnt1;
// 	     // $pcnt1; ":"; $cnt; ":"; $i3;
//              if [($pcnt>0) and ($pcnt<$cnt)] {
// 	     // "hhhhhhhhhhhh";
// 		copy-of $lbracket_s; " "; put_positive(#separ=copy-of $and_s,#els=`*[1]/*`,#nr=$pcnt,#i=$i); copy-of $imp_s; 
// 		put_positive(#separ=copy-of $or_s,#els=`*[1]/*`,#nr=`$cnt - $pcnt`,#neg="1",#i=$i); copy-of $rbracket_s; 
// 	     }
//              else { if [($i3="1") and ($pcnt=0)] { copy-of $lbracket_s; " "; put_positive(#separ=copy-of $or_s,#els=`*[1]/*`,#nr=$cnt,#neg="1",#i=$i); copy-of $rbracket_s; }
//	     if [$i3="1"  and (*[1]/*[not(name()="Not")]) and (*[1]/Not)] { "( ( "; 
//	     ilist(#separ=$and_s, #elems=`*[1]/*[not(name()="Not")]`, #i=$i,#pr="1");
//	    " "; copy-of $rbracket_s; copy-of $imp_s; 
//	    copy-of $lbracket_s; " "; ilist(#separ=$or_s, #elems=`*[1]/Not/*[1]`, #i=$i,#pr="1"); " ) )"; }




tpl [And](#i,#pr) { $e1= is_equiv(#el=`.`); 
    if [$e1="1"] { copy-of $lbracket_s; " ";
       apply[*[1]/*[1]/*[1]](#i=$i,#pr="1"); copy-of $equiv_s;
       apply[*[1]/*[1]/*[2]/*[1]](#i=$i); " "; copy-of $rbracket_s; }
    else { // a bit risky
    if [(@pid=$pid_Iff) and (count(*)=2)] {
       $i1= is_impl(#el=`*[1]`);
       if [$i1="1"] { copy-of $lbracket_s; " "; apply[*[1]/*[1]/*[1]](#i=$i,#pr="1"); copy-of $equiv_s; 
			apply[*[1]/*[1]/*[2]/*[1]](#i=$i); " "; copy-of $rbracket_s; }
       else { $i2= is_impl(#el=`*[2]`);
       if [$i2="1"] { copy-of $lbracket_s; " "; apply[*[2]/*[1]/*[2]/*[1]](#i=$i,#pr="1"); copy-of $equiv_s; 
		      apply[*[2]/*[1]/*[1]](#i=$i); " "; copy-of $rbracket_s; }
       else { $i3 = is_impl1(#el=`*[1]`); $i4 = is_impl1(#el=`*[2]`);
       if [($i3 > 0) or ($i4 > 0)] { // select better impl - no, prefer the first
       $which = { if [($i3 = 0)] { "2"; } else { "1"; }}
//		  if [($i4 = 0)] { "1"; } else { 
//		  if [$i3 > $i4] { "2"; } else { "1"; }}}}
       $i5 = { if [$which=1] { $i3; } else { $i4; }}
       for-each [*[position()=$which]] { // " IFF2: "; $which; 
             copy-of $lbracket_s; " ";
	     if [$i5=2] {
		ilist(#separ = $and_s, #elems=`*[1]/*[not(@pid=$pid_Impl_RightNot)]`, #i=$i,#pr="1"); copy-of $equiv_s; 
		apply[*[1]/*[@pid=$pid_Impl_RightNot]/*[1]](#i=$i); }
             else { 
	        ilist(#separ = $and_s, #elems=`*[1]/*[position()<last()]`, #i=$i,#pr="1"); copy-of $equiv_s; 
                choose {
		when [$i5=3] { 
		     if [name(*[1]/*[position()=last()]) = "Not"] {
			apply[*[1]/*[position()=last()]/*[1]](#i=$i); } 
			// now Pred, which is antonymous
                     else { apply[*[1]/*[position()=last()]](#i=$i,#not="1"); } }
		when [$i5=4] { 
		     apply[*[1]/*[position()=last()]](#i=$i,#ex="1"); }
		when [$i5=5] { 
		     copy-of $not_s; apply[*[1]/*[position()=last()]](#i=$i); }
                }} " "; copy-of $rbracket_s;
	}}		      
       else { copy-of $lbracket_s; " "; comment { "HUMANRECFAILED";} ilist(#separ=$and_s, #elems=`*`, #i=$i,#pr="1"); " "; copy-of $rbracket_s; }}}}
    else { copy-of $lbracket_s; " "; // if[not(@pid)] { " NOPID ";} 
           ilist(#separ=$and_s, #elems=`*`, #i=$i,#pr="1"); " "; copy-of $rbracket_s; }}}

tpl [Pred](#i,#not,#pr) 
{
    choose 
    {
      when [@kind='P'] 
      { 
         pschpvar(#nr=`@nr`); 
	 "["; ilist(#separ=",", #elems=`*`, #i = $i); "]";
      }
      when [(@kind='V') or (@kind='R')]  
      { 
	   $pi = { patt_info(#k=`@kind`, #nr=`@nr`, #pid =`@pid`); }
	   $fnr = car(#l=$pi);
	   $antonym = cadr(#l=$pi);
	   $plink = third(#l=$pi);
	   $pid = { if [$plink="1"] { `@pid`; } else { "0";} }
	   $predattr = { if [$antonym>1] { "1";} else { "0"; }}
	   $neg = { if [$not="1"] { `($antonym + $not) mod 2`; }
		    else { `$antonym mod 2`; }}
           if [$neg="1"] { copy-of $not_s;}
           if [(@kind='V') and ($predattr="0")] 
       	   {
	       apply[*[position() = last()]](#i = $i); copy-of $is_s;  
	       pp(#k=`@kind`,#nr=`@nr`,#args=`*[position() < last()]`,#pid=`@pid`,#i=$i);
	       // abs(#k=`@kind`, #nr=`@nr`, #sym=abs1(#k=`@kind`, #nr=`@nr`, #fnr=$fnr, #pid=$pid)); 
           }
           else { pp(#k=`@kind`,#nr=`@nr`,#args=`*`,#pid=`@pid`,#i=$i); }
      } 
    }
}
//,#sym1=abs(#k=`@kind`, #nr=`@nr`, #sym=abs1(#k=`@kind`, #nr=`@nr`))); }}
//  "[ "; list(#separ=",", #elems=`*`); "]"; }


tpl [PrivPred](#i,#pr,#not) { if [$not="1"] { copy-of $not_s; } pppred(#nr=`@nr`); "["; 
    ilist(#separ=",", #elems=`*[position() < last()]`, #i = $i); "]"; }
tpl [Is](#i,#pr,#not) { apply[*[1]](#i = $i); copy-of $is_s; if [$not="1"] { copy-of $not_s; } apply[*[2]](#i = $i); } 
tpl [Verum](#i,#pr,#not) { if [$not="1"] { "contradiction"; } else { "verum";} }
tpl [ErrorFrm](#i,#pr,#not) { if [$not="1"] { copy-of $not_s; } "errorfrm"; }

tpl [FlexFrm](#i,#pr,#not)
{ 
   $conn = { if [$not="1"] { $or_s; } else { $and_s; } }
   apply[*[1]](#i = $i, #pr = $pr, #not = $not); 
   $conn; copy-of $dots_s; $conn; 
   apply[*[2]](#i = $i, #pr = $pr, #not = $not);
} 

// Terms
// #p is the parenthesis count
// #i is the size of the var stack
tpl [Var](#p,#i) { 
    if [$print_identifiers > 0]
    {
      $vid = { get_vid(#up = `$i - @nr`); }
      pqvar(#nr = `@nr`, #vid = $vid);
    }
    else { pvar(#nr=`@nr`); } 
}

// search parent For and Fraenkel for #nr, return its vid
// #bound says how many vars ( -1) are currently quantified
// (depth of the quantifier stack), so we need to go 
// #bound - #nr times up (this is now passed just as #up)
tpl get_vid(#up) {
    if [name() = "For"] {
       if [$up = "0"] { `@vid`; }
       else { for-each [..] { get_vid(#up = `$up - 1`); } } 
    }
    else { 
    if [(name() = "Typ") and (name(..) = "Fraenkel")] {
       // the case for var inside fraenkel typ - 
       // only previous lamdaargs are available
       $tnr = `count(preceding-sibling::Typ)`;
       if [$up < $tnr] { 
          `preceding-sibling::Typ[position() = (last() - $up)]/@vid`; }
       else { for-each [../..] { get_vid(#up = `$up - $tnr`); } }
    }
    else {
    if [name() = "Fraenkel"] {
       // the case for var inside lambdaterm and lambdaformula -
       // all lamdaargs are available
       $tnr = `count(Typ)`;
       if [$up < $tnr] { 
          `Typ[position() = (last() - $up)]/@vid`; }
       else { for-each [..] { get_vid(#up = `$up - $tnr`); } }
    }
    else { for-each [..] { get_vid(#up = $up); } } } } 
}


// trickery to translate loci to constants and identifiers when needed
// this unfortunately does not work for IdentifyRegistration, so that's
// dealt with by looking at the compatibility fla now :-(
// ###TODO: also the constructor types
tpl [LocusVar](#p, #i) 
{ 
    // try definienda possibly containing "it"
    if [($mml="0") and (ancestor::DefMeaning)]
    {
       $it_possible = { if [(ancestor::Definiens[(@constrkind="M") or (@constrkind="K")])]
		        { "1"; }
			else { "0"; } }

       $maxnr = { for-each [ancestor::Definiens] { `count(Typ)`;} }

       if [(@nr = $maxnr) and ($it_possible="1")] 
       { 
          pkeyword(#str="it"); 
       }
       else 
       {
          if [@nr <= $maxnr] 
	  {
	     $nr = `@nr`;
	     // preceding-sibling written this way selects in reverse document order
	     for-each [ancestor::Definiens]
	     {
	        $argtypes = `preceding-sibling::DefinitionBlock[1]/Let/Typ`;
		ppconst(#nr = $nr, #vid = `$argtypes[position() = $nr]/@vid`);
             }
	  }
	  else 
	  { 
	     ploci(#nr = `@nr`); 
	  }
       }
    }
    else 
    {
       // note that the Constructor may come from different document here
       // even if $mml = 0, but that can be handled above, because this is
       // only used for result types which in that case shouldn't have changed
       // Exapnsion used for expandable mode defs
       if [($mml="0") and ((ancestor::Constructor) or (ancestor::Expansion)) and (ancestor::Definition)]
       {
          $nr = `@nr`;
	  $argtypes = `ancestor::DefinitionBlock/Let/Typ`;
	  ppconst(#nr = $nr, #vid = `$argtypes[position() = $nr]/@vid`);
       }
       else 
       {
          if [($mml="0") and (ancestor::Registration)]
	  {
             $nr = `@nr`;
	     $argtypes = `ancestor::RegistrationBlock/Let/Typ`;
	     ppconst(#nr = $nr, #vid = `$argtypes[position() = $nr]/@vid`);
	  }
	  else 
	  {
	     if [($mml="0") and ((ancestor::DefPred) or (ancestor::DefFunc))]
	     { 
	        "$"; `@nr`;
             }
	     else 
	     { 
                ploci(#nr = `@nr`); 
	     }
	  }
       }
    }
}

tpl [FreeVar](#p,#i) { "X"; `@nr`; }
tpl [Const](#p,#i) 
{ 
    if [($print_identifiers > 0)  and ((@vid>0) or ($proof_links>0))]
    {
       if [@vid > 0]
       {
          $pl = { if[$const_links=2]  { get_nearest_level(#el = `..`); } }
          ppconst(#nr = `@nr`, #vid = `@vid`, #pl = $pl);
       } 
       else    
       {
          $pl = get_nearest_level(#el = `..`); 
	  absconst(#nr = `@nr`, #pl = $pl);
       }
    }
    else 
    { 
       pconst(#nr = `@nr`); 
    }
}
tpl [InfConst](#p,#i) { "D"; `@nr`; }
tpl [Num](#p,#i) {  `@nr`; }
tpl [Func](#p,#i) { 
    choose {
      when [@kind='F'] { pschfvar(#nr=`@nr`); 
	   copy-of $lbracket_s; ilist(#separ=",", #elems=`*`, #i = $i); copy-of $rbracket_s;}
      when [@kind='U'] { copy-of $the_sel_s;
        abs(#k=`@kind`, #nr=`@nr`, #sym=abs1(#k=`@kind`, #nr=`@nr`));
        copy-of $of_sel_s; apply[*[position() = last()]](#p = $p, #i = $i); }
      otherwise { 
        $par = { if [$p>0] { `$p+1`;} else { 
                 if [name(..)='Func'] { "1"; } else { "0";} }  }
        pp(#k=`@kind`,#nr=`@nr`,#args=`*`,#parenth=$par,#pid=`@pid`,#i=$i); }}} 

tpl [PrivFunc](#p,#i) { ppfunc(#nr=`@nr`); copy-of $lbracket_s; 
    ilist(#separ=",", #elems=`*[position()>1]`, #i = $i); copy-of $rbracket_s; }
tpl [ErrorTrm](#p,#i) { "errortrm"; }
tpl [Choice](#p,#i) { copy-of $choice_s; apply[Typ](#i = $i); }
tpl [Fraenkel](#p,#i) {
    $j = { if [$i] { $i;} else { "0"; } }
    $par = { if [$p>0] { `$p+1`;} else { "1"; } }
    $inc = { `count(*) - 2`; } // number of vars introduced here
    $paren_color = `$par mod $pcolors_nr`;
     <span { @class=`concat("p",$paren_color)`; copy-of $fraenkel_start; 
       <span { @class="default"; " ";
         // first display the term
         apply[*[position() = last() - 1]](#p = $par, #i = `$j + $inc`); 
	 // then the var types
         if  [count(*)>2] 
	 { 
	     " where ";  
	     for-each[*[position() < last() - 1]] 
	     {
		pqvar(#nr = `$j + position()`, #vid = `@vid`);
		$eq1 = { if [position()=last()] { "0"; } else {
			    are_equal_vid(#el1=`.`,#el2=`following-sibling::*[1]`); } }
		if [$eq1="0"]  {  copy-of $is_s; apply[.](#i=`$j + position() - 1`); }
                if [not(position()=last())] { ", "; }
              }
          }
	 // then the formula
         " : "; apply[*[position() = last()]](#i = `$j + $inc`); " "; }
       copy-of $fraenkel_end; } " ";
 }

// Types
// element Typ {
//    attribute kind { "M" | "G" | "L" | "errortyp" },
//    attribute nr { xsd:integer }?,
//    ( attribute absnr { xsd:integer },
//      attribute aid { xsd:string } )?,
//    attribute pid { xsd:integer }?,
//    Cluster*,
//    Term*
//  }
tpl [Typ](#i) 
{ 
   " ";
   if [count(*)>0] { apply[*[1]](#i = $i); }
   if [(@kind="M") or (@kind="G") or (@kind="L")] 
   { 
      $pi     = { patt_info(#k = `@kind`, #nr = `@nr`, #pid = `@pid`); }
//DEBUG ":"; `@pid`; ":"; $pi; ":";
      $fnr    = car(#l = $pi);
      $expand = cadr(#l = $pi);
      $plink  = third(#l = $pi);
      $k1     = { if [@kind = "M"] { "M"; } else { "L";} }

      if [($expand="0") or not(@pid)] 
      {
         pp(#k = $k1, #nr = `@nr`, #args = `*[not(name()="Cluster")]`,
            #pid = `@pid`, #i = $i);
      }
      else 
      {
         $sym = abs1(#k = `@kind`, #nr = `@nr`, #fnr = $fnr);
	 $vis = cdddr(#l = $pi); 
	 $el  = `.`;  //DEBUG ":"; `@pid`; ":"; $pi; ":";
	 $pid = `@pid`;
	 $doc = { if [key('EXP',$pid)] { ""; } else { $patts; } }
	 $c1  = { if [($doc = "") and ($mml = "0")] { "1"; } else { "0"; } }

	 for-each [document($doc,/)] 
	 { 
	    absref(#elems = `key('EXP',$pid)`, #c = $c1, #sym = $sym, #pid = $pid);
	    if [not($vis = "")] 
	    { 
	       $of_typ_s;
	       for-each [key('EXP',$pid)] 
	       {
	          descent_many_vis(#patt = `Expansion/Typ`, #fix = $el, 
			           #vis = `Visible/Int`, #i = $i); 
               }
            }
         }
      }
   }
   else { `@kind`; }
}

// Gets two Typ (#patt and #fix), and a list of Visible/Int .
// Tries to find and print the terms in #fix corresponding
// to the visible loci; #patt is structurally similar to
// #fix, up to the loci .
// The handling of #i is potentially incorrect if there is a Fraenkel as 
// a param of the type .
// Newly we also descent through Clusters, because dependent adjectives
// allow things like: mode ManySortedSet of I is  I -defined total Function .
// We still optimize by starting with the terms (after "of"), the clusters
// are used last (if nothing was found in terms).
tpl descent_many_vis(#patt,#fix,#vis,#i)
{ 
  if [$vis] 
  {
    $v1= `$vis[position()=1]/@x`;
    $v2= `$vis[position()>1]`;
    $adjnrs = { for-each [$patt/Cluster[1]/Adjective] { ":"; `@nr`; ":"; } }
//DEBUG    "descen:"; $v1; ":"; apply[$patt]; ":"; 
    descent_many(#patts = `$patt/*[(not(name()="Cluster"))] | $patt/Cluster[1]/Adjective`,
		 #fixs  = `$fix/*[(not(name()="Cluster"))] | $fix/Cluster[1]/Adjective[(contains($adjnrs, concat(":",@nr,":")))]`,
		 #lnr   = $v1,
		 #nr    = `count($patt/*[(not(name()="Cluster"))]) + count($patt/Cluster[1]/Adjective)`,
		 #i     = $i); 
    if [$v2] { ","; descent_many_vis(#patt=$patt,#fix=$fix,
		    #vis=`$vis[position()>1]`, #i = $i); }
  }
}

tpl descent_many(#patts,#fixs,#lnr,#nr,#i)
{ 
  if [$nr > 0] 
  {
    $patt=`$patts[position()=$nr]`;
    $fix =`$fixs[position()=$nr]`;
//DEBUG "desone:"; $nr; ":"; `name($patt)`; ":"; `name($fix)`; ":";
    if [(name($patt)="LocusVar") and ($patt/@nr=$lnr)] { 
//DEBUG    $lnr; ":"; `$patt/@nr`; ":";  "fff";
	  for-each [$top] { apply[$fix](#p="0", #i = $i); } } 
// the duplication here is needed to generated the html properly;
// it does not cause any visible slowdown in practice
    else { $res= { if [name($patt) = name($fix)] { 
		      descent_many(#patts=`$patt/*`,#fixs=`$fix/*`,
				   #lnr=$lnr,#nr=`count($patt/*)`, #i = $i);  } 
                   else {"";}} 
      if [$res and not($res="")] {
//DEBUG [and contains($res,"fff")]
	  descent_many(#patts=`$patt/*`,#fixs=`$fix/*`,
		      #lnr=$lnr,#nr=`count($patt/*)`, #i = $i);  }
      else 
      { descent_many(#patts=$patts,#fixs=$fixs,#lnr=$lnr,#nr=`$nr - 1`, #i = $i); }}
  }
}

// Clusters
// only attributes with pid are now printed, unless %all=1;
// others are results of 
// cluster mechanisms - this holds in the current article 
// (.xml file) only, environmental files do not have the @pid 
// info (yet), so we print everything for them
tpl [Cluster](#i,#all) 
{ 
   if [($print_all_attrs = 1) or ($all = 1)]
   {
      list(#separ=" ", #elems=`*`);
   }
   else
   {
      list(#separ=" ", #elems=`*[@pid]`);
   }

   " "; 
}

// Adjective
//  element Adjective {
//    attribute nr { xsd:integer },
//    attribute value { xsd:boolean }?,
//    ( attribute absnr { xsd:integer },
//      attribute aid { xsd:string } )?,
//    attribute kind { "V" }?,
//    attribute pid { xsd:integer }?,
//    Term*
//  }
tpl [Adjective](#i) 
{ 
     $pi    = { patt_info(#k="V", #nr=`@nr`, #pid =`@pid`); }
     $fnr   = car(#l = $pi);
     $anto  = cadr(#l = $pi);
     $plink = third(#l = $pi);

     $pid   = { if [$plink="1"] { `@pid`; } else { "0";} }
     $neg   = { if [@value="false"] { `($anto + 1) mod 2`; } else { `$anto mod 2`; }}

     if [$neg="1"] 
     { 
        copy-of $non_s;
     }

     pp(#k="V",#nr=`@nr`,#args=`*`,#pid=`@pid`,#i=$i);
//     abs(#k="V", #nr=`@nr`,#sym=abs1(#k="V", #nr=`@nr`, #fnr=$fnr, #pid=$pid), #pid = $pid); 
}



//
// File: print_complex.xsltxt - html-ization of Mizar XML, more complex printing stuff
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)


// article references
// add the reference's href, $c tells if it is from current article
// $nm passes the explicit text to be displayed
tpl aidref(#aid) 
{
  $alc =  { lc(#s = $aid); }
  <a {
      @class = "ref";

      if [($linking = 'q') or (($linking = 'm') and not($c))] 
      {
        @href = `concat($mmlq,$aid)`;
      }
      else 
      {
        @href =	
	{
           if[($aid = $aname) and (($linking = 'm') or ($linking = 'l'))]
	   {
	      "#";
	   }
	   else { `concat($mizhtml,$alc, ".",$ext)`; }
	}

        if [$aid = $aname] 
	{
          @target = "_self";
        }
      }

      $aid;
 }
}
   
// ##TODO: try some unification of mkref and absref
//
// theorem, definition and scheme references
// add the reference's href, $c tells if it is from current article
// $nm passes the explicit text to be displayed
tpl mkref(#aid, #nr, #k, #c, #nm) 
{
  $mk  =  { refkind(#kind = $k); }
  $alc =  { lc(#s = $aid); }
  <a {
      @class = "ref";

      if [($linking = 'q') or (($linking = 'm') and not($c))] 
      {
        @href = `concat($mmlq,$aid,":",$mk,".",$nr)`;
      }
      else 
      {
        @href =	
	{
           if[($c = 1) and (($linking = 'm') or ($linking = 'l'))]
	   {
	      `concat("#",$k, $nr)`;
	   }
	   else { `concat($mizhtml,$alc, ".",$ext, "#",$k, $nr)`; }
	}

        if [$c = "1"] 
	{
          @target = "_self";
        }
      }

      if [$ref_tooltips="1"]
      { 
         // quick hack for MizAR; should get the local ones from the DOM
	 // we use ($mk_ajax_refs > 0) as the confirmation that local refs are produced
	 if[(not($c = "1")) or ($mk_ajax_refs > 0)]
	 {
           @onmouseover=`concat("rs('",$alc, "/", $k, $nr, "')")`; 
      	   @onmouseout="rh()"; 
         }
      }

      if [$titles="1"] 
      {
         // no title if there is a tooltip
	 if[not($ref_tooltips="1") or (($c = "1") and not($mk_ajax_refs > 0))]
	 {
           @title = `concat($aid,":",$mk,".",$nr)`;
         }
      }

      if [$nm] 
      { 
        $nm; 
      }
      else 
      {
        $aid; ":";

        if [not($k="T")] 
	{
          $mk; " ";
        }

        $nr;
      }

    }
}




// add the constructor/pattern href, $c tells if it is from current article
// #sym is optional Mizar symbol
// #pid links to  patterns instead of constructors
tpl absref(#elems, #c, #sym, #pid)
{ 
   $n1 = { if [($pid > 0)] { "N"; } else { ""; } }

   for-each [$elems] 
   { 
      $mk0  = mkind(#kind = `@kind`); 
      $mk   = { if [($pid > 0)] { `concat($mk0, "not")`; } else { $mk0; } }
      $alc  = lc(#s=`@aid`);

      <a 
      { 
         if [($linking = 'q') or (($linking = 'm') and not($c = "1"))] 
	 { 
	    @href = `concat($mmlq,@aid,":",$mk,".",@nr)`;
	 }
	 else 
	 { 

            @href =	
	    {
               if[($c = 1) and (($linking = 'm') or ($linking = 'l'))]
	       {
	          `concat("#", $n1, @kind, @nr)`;
	       }
	       else { `concat($mizhtml,$alc, ".",$ext, "#", $n1, @kind, @nr)`; }
	    }

	    // this is probably needed if $mml = 1
	    if [($c = "1") and not($linking = "s")] { @target="_self"; } 
         }

	 if [$titles="1"] 
	 { 
	    $t1 = { if [$pid > 0] { `@kind`; } else { $mk; } }
	    @title=`concat(@aid, ":", $n1, $t1, ".", @nr)`; 
         }

	 if [$sym] 
	 { 
	    $sym; 
	 }
	 else 
	 { 
	    if [$relnames > 0]
	    { 
	       $n1; `@kind`; `@relnr`; 
	    }
	    else 
	    { 
	       $n1; `@kind`; `@nr`; "_"; `@aid`;  
	    } 
	 }
      }
   } 
}

// look up and link the constructor/pattern with kind #k and #nr;
// #sym is optionally forces the given Mizar symbol
// #pid links to  patterns instead of constructors
// note that we can be inside a Notation document here already (see pp),
// so the $doc = "" test does not have to mean that we are inside
// the article (could be probably fixed in pp, don't know about expnadable modes though)
tpl abs(#k, #nr, #sym, #pid) 
{
   if [$pid>0] 
   {
      $k1  = `concat('P_',$k)`;
      $doc = { if [key($k1,$nr)[$pid=@relnr]] { ""; } else { $patts; } }

      for-each [document($doc,/)] 
      {
         $c1  = { if [(name(/*) = "Article") and ($mml = "0")] { "1"; } else { "0"; } }
         absref(#elems = `key($k1,$nr)[$pid=@relnr]`, #c = $c1, #sym = $sym, #pid = $pid);
      }
   } 
   else 
   {
      $doc = { if [key($k,$nr)] { ""; } else { $constrs; } }

      for-each [document($doc,/)] 
      {
         $c1  = { if [(name(/*) = "Article") and ($mml = "0")] { "1"; } else { "0"; } }
         absref(#elems = `key($k,$nr)`, #c = $c1, #sym = $sym);
      }
   }
}

// pretty printer - gets arguments, visibility info from pattern,
// format telling arities, the linked symbol and optionally right bracket
// parenth hints to put the whole expression in parentheses, but this
// is overrriden if the expression uses functor brackets
// #loci tells to print loci instead of arguments
// #i is the bound var nbr
tpl pp(#k, #nr, #args, #parenth, #pid, #loci, #i) 
{
  $pkey = `concat('P_',$k)`;

  //  pattern number given 
  if [$pid>0] 
  {
     $doc     = { if [key($pkey,$nr)[$pid=@relnr]] { ""; } else { $patts; } }

     for-each [document($doc,/)] 
     {
         if [key($pkey,$nr)[$pid=@relnr]] 
	 {
	    for-each [key($pkey,$nr)[$pid=@relnr]] 
	    {
	       $npid =  { if [@redefnr>0] { $pid; } }
	       // $vis = { if [$k = "V"] { `Visible/Int[position() < last()]`; } else { `Visible/Int`; } }

	       if [$k = "V"] 
	       { 
	          pp1(#k = $k, #nr = $nr, #args = $args, #vis = `Visible/Int[position() < last()]`,
	              #fnr = `@formatnr`, #parenth = $parenth, #loci = $loci, #pid = $npid, #i = $i);
	       }
	       else 
	       {
	       	  pp1(#k = $k, #nr = $nr, #args = $args, #vis = `Visible/Int`,
	              #fnr = `@formatnr`, #parenth = $parenth, #loci = $loci, #pid = $npid, #i = $i);
	       }

            }
	 }
	 //  failure, print in absolute notation 
	 else 
	 {
	    abs(#k = $k, #nr = $nr);
	    "(";
	    list(#separ = ",", #elems = $args);
	    ")";
	 }
     }
  }
  //  pattern number not given - take first suitable 
  else 
  {
     $doc     = { if [key($pkey,$nr)] { ""; } else { $patts; } }

     for-each [document($doc,/)] 
     {
         if [key($pkey,$nr)] 
	 {
	    for-each [key($pkey,$nr)[position()=1]] 
	    {
               $npid =  { if [@redefnr>0] { `@relnr`; } }
//	       $vis = { if [$k = "V"] { `Visible/Int[position() < last()]`; } else { `Visible/Int`; } }
  	       if [$k = "V"] 
	       { 
	         pp1(#k = $k, #nr = $nr, #args = $args, #vis = `Visible/Int[position() < last()]`,
	             #fnr = `@formatnr`, #parenth = $parenth, #loci = $loci, #pid = $npid, #i = $i);
	       }
	       else 
	       {
	       	 pp1(#k = $k, #nr = $nr, #args = $args, #vis = `Visible/Int`,
	             #fnr = `@formatnr`, #parenth = $parenth, #loci = $loci, #pid = $npid, #i = $i);
	       }
            }
         }
	 //  failure, print in absolute notation 
	 else 
	 {
	    abs(#k = $k, #nr = $nr);
	    "(";
	    list(#separ = ",", #elems = $args);
	    ")";
         }
      }
   }
}




// it is legal to pass only #loci instead of #args here
// #pid is passed to abs, causes linking to patterns
// #i is the bound var nbr
tpl pp1(#k,#nr,#args,#vis,#fnr,#parenth,#loci,#pid,#i) 
{
    $la = { if [($k='M') or ($k='G') or ($k='L')] {  "0"; } 
            else { for-each [document($formats,/)] {
                     for-each [key('F',$fnr)] 
		     { 
		       choose
		       { 
		         when [@kind="V"] { `@argnr - 1`;}
                         when [@leftargnr] { `@leftargnr`;} 
			 otherwise { "0";} 
                       }
                     }}} 
          }
    // try if right bracket - returns '' if not
    $rsym = { if [($k='K') and ($la='0')] { abs1(#k=$k, #nr=$nr, #fnr=$fnr, #r="1"); } }
    $np = { if [not($vis) or ($k='G')] { "0"; } else {
               if [$parenth>0] { $parenth; } else { 
                  if [not($rsym='')] { "1"; } else { "0";} } } }
    $paren_color = `$np mod $pcolors_nr`;

    // print spanned paranthesis or left bracket
    if [($parenspans = 1) and ($np > 0)] 
    { 
       <span 
       { 
          @class=`concat("p",$paren_color)`;

	  if [$rsym=''] 
	  { 
	     "("; 
	  } 
	  else 
	  { 
             abs(#k=$k, #nr=$nr, #sym=abs1(#k=$k, #nr=$nr, #fnr=$fnr), #pid=$pid); 
	  }

	  <span 
	  { 
             @class="default";
	     pp2(#k = $k, #nr = $nr, #i = $i, #vis = $vis, #la = $la, #loci = $loci, #args = $args, 
	         #np = $np, #rsym = $rsym, #parenth = $parenth, #fnr = $fnr, #pid = $pid);
          }

	  if [$rsym=''] { ")"; } else { abs(#k=$k, #nr=$nr, #sym=$rsym, #pid=$pid); } 
       }
    } 
    else 
    {
       if[($np > 0)]
       {
          if [$rsym=''] { "("; } 
	  else 
	  { 
             abs(#k=$k, #nr=$nr, #sym=abs1(#k=$k, #nr=$nr, #fnr=$fnr), #pid=$pid); 
	  }
       }

       pp2(#k = $k, #nr = $nr, #i = $i, #vis = $vis, #la = $la, #loci = $loci, #args = $args, 
           #np = $np, #rsym = $rsym, #parenth = $parenth, #fnr = $fnr, #pid = $pid);

       if[($np > 0)]
       {
          if [$rsym=''] { ")"; } else { abs(#k=$k, #nr=$nr, #sym=$rsym, #pid=$pid); }
       }
    }
}

tpl pp2(#k, #nr, #i, #vis, #la, #loci, #args, #np, #rsym, #parenth, #fnr, #pid)
{
   $visnr = `count($vis)`;

   $dofuncbrackets = { if [($rsym='') and ($mizar_brackets > 0) and ($k = "K")] { "1"; } else { "0"; } }

   if [($dofuncbrackets>0) and ($la>1)] { "("; } 

   // print left args
   for-each [$vis] 
   { 
      if [position() <= $la] 
      {
	$x=`@x`;
	if [$loci>0] 
	{ 
	   if [$loci="2"] 
	   { 
	      ppconst(#nr=$x,#vid=`$args[position()=$x]/@vid`); 
	   } 
	   else { ploci(#nr=$x); }
        }
	else { apply[$args[position() = $x]](#p=$np,#i=$i); }
	if [position() < $la] { ",";} 
      } 
   }

   if [($dofuncbrackets>0) and ($la>1)] { ")"; }
 
   // print symbol
   if [$rsym=''] 
   {
      // only consider printing space if $parenth was not printed or there were left args
      // there were left arg(s), and $dofuncbrackets>0 (we are inside a functor), the left arg(s) will have brackets
      // then if $funcs_no_spaces>0 don't do the space 
      if [not($parenth>0) or ($la>0)] { 
      // do not print space if either:
      // opening parenth was printed and no left args exist
      // or
      // $la>1 and we do func brackets (that means a closing bracket of args was printed)
      // or $la=1 and the left arg got its own parenth (this si implied by $parenth>0)
      if [not(($k='K') and ($parenth>0) and ($la=0)) 
      	  and not(($funcs_no_spaces>0) and ($dofuncbrackets>0) and ($la>0))] {" "; } } 
      abs(#k=$k, #nr=$nr, #sym=abs1(#k=$k, #nr=$nr, #fnr=$fnr), #pid=$pid); 
      if [$k='G'] { "(#"; } 
      // do not print space if either:
      // closing parenth will be printed and no right args exist
      // or
      // $ra>1 and we do func brackets (that means an opening bracket of args will be printed)
      if [not(($k='K') and ($parenth>0) and (($visnr - $la)=0)) 
          and not(($funcs_no_spaces>0) and ($dofuncbrackets>0) and (($visnr - $la)>0))] {" "; } 
   }

   if [($dofuncbrackets>0) and (($visnr - $la)>1)] { "("; } 

   // print right args preceded by "of" for types
   for-each [$vis] 
   { 
      if [(position() = 1)] 
      { 
         if[($k='M')] { "of "; } else { if [($k='L')] { "over "; } }
      }
      if [position() > $la] 
      {
	$x=`@x`;
	if [$loci>0] 
	{ 
	   if [$loci="2"] 
	   { 
	      ppconst(#nr=$x,#vid=`$args[position()=$x]/@vid`); 
           } 
	   else { ploci(#nr=$x); }
        }
	else { apply[$args[position()  = $x]](#p=$np,#i=$i); }
     if [position() < last()] { ",";} } 
   }
   if [$k='G'] { " #)"; } 
   if [($dofuncbrackets>0) and (($visnr - $la)>1)] { ")"; } 
}


// theorem, definition and scheme references
tpl getref(#k, #anr, #nr) 
{
  if [$anr>0] 
  {
    $refdoc = { if [$k="S"] { $schms; } else { $thms; } }

    for-each [document($refdoc,/)] 
    {
      for-each [key($k,concat($anr,':',$nr))[position()=1]] 
      {
         mkref(#aid = `@aid`, #nr = $nr, #k = $k);
      }
    }
  }
  else 
  {
     mkref(#aid = $aname, #nr = $nr, #k = $k, #c = "1");
  }
}

// find the constant with #nr on level #pl or higher,
// and pretty print it
// now assumes that proof levels are available, which is only through
// addabsrefs preprocessing
tpl absconst(#nr,#pl) 
{
   if [key("C",$pl)[@nr = $nr]] 
   { 
      for-each [key("C",$pl)[@nr = $nr]] 
      {
         ppconst(#nr = $nr, #vid = `Typ[position() = 1]/@vid`); 
      }
   }
   else 
   { 
      if [key("C",$pl)[@nr < $nr]] 
      { 
         for-each [key("C",$pl)[@nr < $nr]] 
         { 
            if [position() = last()] 
	    {
      	       $n1     = getcnr(#el = `.`); 
	       $lastnr = `@nr + $n1 - 1`; 
	       $n2     = `@nr`;

	       if [$lastnr >= $nr] 
	       { 
      	          ppconst(#nr = $nr, #vid = `Typ[position() = ($nr - $n2 + 1)]/@vid`); 
      	       }
	       else 
	       { 
      	          $dbgmsg;
	       }
      	    }
         }
      }
      else 
      {
         $ls = `string-length($pl)`;

         if [$ls>0] 
         { 
            $pl1 = { get_parent_level(#pl = $pl, #ls = $ls, #n = "1"); }
	    absconst(#nr = $nr, #pl = $pl1); 
         } 
         else 
         { 
	    $dbgmsg; 
         }
      }
   }
}
//
// File: reasoning.xsltxt - html-ization of Mizar XML, code for reasoning items
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)



tpl [Proposition] 
{ 
    if [$proof_links>0] {<a { @NAME=propname(#n=`@propnr`, #pl=`@plevel`); }}

    if [following-sibling::*[1][(name()="By") and (@linked="true")]] 
    { 
       if [not((name(..) = "Consider") or (name(..) = "Reconsider") 
           or (name(..) = "Conclusion"))] 
       { 
          pkeyword(#str="then "); 
       }
    }

    if [@nr>0] 
    { 
       if [($proof_links>0) and ($print_lab_identifiers = 0) 
            and not(string-length(@plevel)>0)]
       { 
	  plab1(#nr=`@nr`,#txt="Lemma"); 
       }
       else { pplab(#nr=`@nr`, #vid = `@vid`); }

       ": ";
    }

    // ###TODO: include the possible link when generating items
    if [($generate_items>0) and not(string-length(@plevel)>0)] 
    { 
       if [name(..) = "SchemeBlock"] { apply; " "; }
       else
       {
         if [not(name(..) = "SchemePremises")]
	 {
	   pcomment(#str = `concat($aname, ":lemma ", @propnr)`);
         }
	 apply; " "; 
	 if [($generate_items_proofs>0) and
	      (following-sibling::*[1][(name()="By") or (name()="From") or (name()="Proof")])] 
	 { 	 
	   apply[`following-sibling::*[1]`]; 
	 }
       }
    }
    // we can only say that this is a lemma if it is a toplevel proposition
    // nontoplevel could be assumptions, etc. - this is a ##TODO
    else { if [not(string-length(@plevel)>0)] 
    {
       <span { @about=`concat("#E",@propnr)`; @typeof="oo:Lemma"; apply; " "; }
    }
    else { apply; " ";} 
    }
}

tpl mk_by_title(#line, #col) { `concat("Explain line ", $line, " column ", $col)`; }

// Justifications
tpl linkbyif(#line,#col,#by) 
{ 
   if [$linkby>0] 
   { 
      $byurl = 
      { 
         choose 
	 { 
	    when [$linkby=1] { `concat($lbydir,$anamelc,"/",$line,"_",$col,".html")`; }
	    when [$linkby=2] { `concat($lbydlicgipref,$anamelc,"/",$line,"_",$col,".dli")`; } 
	    when [$linkby=3] { `concat($lbytptpcgi,"?article=",$anamelc,"&lc=",$line,"_",$col,"&tmp=",$lbytmpdir,$lbycgiparams)`; } 

	 } 
      }

      <a { 
            if[$ajax_by > 0] { add_ajax_attrs(#u=$byurl); }
	    else
	    {
	       @href=$byurl; @class="txt"; 
	       if[$linkbytoself > 0] {@target="_self"; } else {@target="byATP";} 
            }
	    if [$by_titles>0] { @title=mk_by_title(#line=$line,#col=$col); }
	    pkeyword(#str=$by); " ";  
	 }
      if[$ajax_by > 0] { <span { " "; } } 
    }
    else { pkeyword(#str=$by); " ";  }
}

// if #nbr=1 then no <br; is put in the end 
// (used e.g. for conclusions, where definitional 
//  expansions are handled on the same line)
tpl [By	](#nbr) 
{ 
   if [(count(Ref)>0)] 
   { 
      linkbyif(#line = `@line`, #col = `@col`,#by = "by");
      <span { @class="lab"; list(#separ = ", ", #elems = `Ref`); } 
      ";"; 
   }
   else 
   { 
      if [$linkby>0] {  linkbyif(#line = `@line`, #col = `@col`,#by = ";"); }
      else { ";"; }
   }

   if [not($nbr = "1")] { <br;  }
}

tpl [IterStep/By] { if [(count(Ref)>0)] { 
      linkbyif(#line=`@line`,#col=`@col`,#by="by");
      <span { @class="lab"; list(#separ=", ", #elems=`Ref`); } }}
tpl [From](#nbr) 
{ 
    linkbyif(#line=`@line`,#col=`@col`,#by="from");
    <span 
    { 
        @class="lab";
        getref(#k="S", #anr=`@articlenr`, #nr=`@nr`); "(";
	list(#separ=", ", #elems=`Ref`); ")"; ";"; 
	if [not($nbr="1")] { <br;  } 
    } 
}
tpl [IterStep/From] 
{ 
   linkbyif(#line=`@line`,#col=`@col`,#by="from");
   <span { @class="lab"; getref(#k="S", #anr=`@articlenr`, #nr=`@nr`); "(";
        list(#separ=", ", #elems=`Ref`); ")"; } 
}


// ##REQUIRE: the following two can be called only if $proof_links>0
tpl top_propname(#el) 
{ 
   for-each [$el/..] 
   {
      if [(name() = "DefTheorem") or (name() = "JustifiedTheorem")] 
      {
         $k = { if [@kind='D'] { "Def"; } else { "Th"; } }

         $nm = 
	 { 
	    if [($print_lab_identifiers > 0) and ($el/@vid > 0)] { get_vid_name(#vid = `$el/@vid`); }
	    else { `concat($k,@nr)`; }
         }

	 mkref(#aid = $aname, #nr = `@nr`, #k = `@kind`, #c = "1", #nm = $nm);
      }
      else 
      { 
         $k1 = `concat($el/@nr,":")`;
	 $k2 = `key("E",$k1)/@propnr`;

	 <a 
	 { 
	    @class = "txt"; 
	    @href  = `concat($anamelc, ".", $ext, "#","E",$k2)`;  
	    if [($print_lab_identifiers > 0) and ($el/@vid > 0)] 
	    { 
	       pplab(#nr = `$el/@nr`, #vid = `$el/@vid`);  
            }
	    else { plab1(#nr = `$el/@nr`, #txt = "Lemma"); }
         }
      }
   }
}


// name of private reference - name of the proposition
tpl privname(#nr,#pl) {
      $k1 = `concat($nr,":",$pl)`;
      if [key("E",$k1)] 
      { 
	 for-each [key("E",$k1)] 
	 {
	    if [not(string-length($pl)>0)] { top_propname(#el = `.`); }
	    else 
	    { 
	      $txt= { propname(#n = `@propnr`, #pl = $pl); } 
	      <a 
	      { 
	         @class = "txt"; 
//		 @href  = `concat($anamelc, ".", $ext, "#",$txt)`;
		 @href  = `concat("#",$txt)`;
		 pplab(#nr=`@nr`, #vid = `@vid`); 
              } 
            }
         } 
      }
      else { 
	   $ls = `string-length($pl)`;
	   if [$ls>0] { 
	      $pl1 = { get_parent_level(#pl=$pl,#ls=$ls,#n="1"); }
	      privname(#nr=$nr,#pl=$pl1); } }
 }


// count local constants introduced in the current element -
// this asssumes Let | Given | TakeAsVar | Consider | Set | Reconsider
tpl getcnr(#el) 
{ 
   `count($el/Typ)`; 
}

// relies on addabsrefs preprocessing
tpl get_nearest_level(#el) 
{ 
   for-each [$el] 
   { 
      if [@newlevel] 
      { 
         `@newlevel`;
      } 
      else 
      { 
         get_nearest_level(#el=`..`); 
      }
   }
}

tpl [Ref] 
{ 
   if [not(@articlenr)] 
   {  
      if [$proof_links = 0] 
      { 
         // experimental!!
	 $n1 = `@nr`;
	 $vid =  
	 { 
	   if [@vid] { `@vid`; }
	   else
	   {
              if [$print_lab_identifiers > 0] // makes things faster if not, cause this is expensive
              { 
//	 for-each [preceding::*[((name()="Proposition") or (name()="Now") or (name()="IterEquality")) and (@nr=$n1)][1]]
//       this seems to be reasonably fast 
	         for-each [(preceding::Proposition[@nr=$n1]|preceding::Now[@nr=$n1]
                           |preceding::IterEquality[@nr=$n1])[last()]]
                 { `@vid`; }
	      }
	      else { "0"; }
           }
         }

         pplab(#nr = $n1, #vid= $vid);
      }
      else 
      { 
         $pl = get_nearest_level(#el = `..`); 
	 privname(#nr = `@nr`, #pl = $pl); 
      }
   }
   else 
   { 
      getref(#k = `@kind`, #anr = `@articlenr`, #nr = `@nr`);
   }
}

tpl [ErrorInf](#nbr) { "errorinference;"; if [not($nbr="1")] { <br;  } }
tpl [IterStep/ErrorInf] { "errorinference"; }
tpl [SkippedProof](#nbr) 
{ 
  if[$ajax_proofs=2] { <span {  @filebasedproofinsert=`@newlevel`;}}
  pkeyword(#str="@proof .. end;"); 
  if [not($nbr="1")] { <br;  } 
}
tpl [IterStep/SkippedProof] { pkeyword(#str="@proof .. end;"); }

//   Term, elIterStep+
tpl [IterEquality](#nbr) 
{ 
   if [IterStep[1]/By[@linked="true"]] 
   {
      if [not(name(..)="Conclusion")] { pkeyword(#str="then ");}
   }

   if [@nr>0] {  pplab(#nr = `@nr`, #vid = `@vid`); ": ";}

   apply[*[1]]; " = ";
   nlist(#separ=".= ", #elems=`IterStep`); ";"; 

   if [not($nbr="1")] { <br;  } 

}

tpl [IterStep] { apply;  }

// Skeleton steps
//tpl [Let] { $j=`@nr`; pkeyword(#str="let "); pconst(#nr=$j);
//             " be "; 
//            jlist(#j=$j, #sep2=" be ", #elems=`*`); 
//	    ";"; try_th_exps(); <br; }

// #fst tells to process in a sequence of Let's
// #beg is the beginning of const. sequence numbers 
tpl [Let](#fst,#beg) { 
  $has_thesis = { if [following-sibling::*[1][name()="Thesis"]] { "1"; }
		  else { "0"; }  }
  $it_step = { if [$has_thesis="1"] { "2"; } else { "1"; }} 
  if // if not first in a sequence, it is already handled - do nothing -
     // this prevents the default proof traversal of already handled Lets 
    [not($fst="1") and (preceding-sibling::*[position()=$it_step][name()="Let"])] {}
  else 
  { // try next Let for the same type - we cannot deal with thesis here 

  $next = 
  { 
     if [(count(Typ)=1) and 
         (following-sibling::*[position()=$it_step][name()="Let"][count(Typ)=1]) and
	 (($has_thesis="0") or 
	  ((following-sibling::*[1][name()="Thesis"][not(ThesisExpansions/Pair)])
	   and
	   (following-sibling::*[3][name()="Thesis"][not(ThesisExpansions/Pair)])))]
     {  
        are_equal_vid(#el1=`./Typ`, #el2=`following-sibling::*[position()=$it_step]/Typ`); 
     }
     else { "0"; }
  }

  if [$beg] // no thesis guaranteed, only one const guaranteed
	    // this sequence has already been started,
   {   
       ", ";
       if [$const_links>0] 
       {   
	     $addpl = { addp(#pl=`@plevel`); } 
	     <a { @NAME=`concat("c",@nr,$addpl)`; }
       } 
       ppconst(#nr = `@nr`, #vid = `Typ/@vid`);
       if [$next="1"] // and does not end here - print the rest
       {
          apply[following-sibling::*[position()=$it_step]](#fst="1",#beg=$beg);
       }
       else // or ends here - print the type, deal with following
       { 
          " be "; apply[Typ]; ";"; try_th_exps(); <br;
	  apply[following-sibling::*[position()=$it_step][name()="Let"]](#fst="1"); 
       }
   }
  else  // start of sequence
   {
       pkeyword(#str="let ");
       if [$next="1"] // not ending here; no thesis guaranteed, only one const guaranteed
       {
          if [$const_links>0] 
	  {   
	     $addpl = { addp(#pl=`@plevel`); } 
	     <a { @NAME=`concat("c",@nr,$addpl)`; }
	  }
	  ppconst(#nr = `@nr`, #vid = `Typ/@vid`);
	  apply[following-sibling::*[position()=$it_step]](#fst="1",#beg=`@nr`);
       }
       else // print them all
       {
          jtlist(#j=`@nr - 1`, #sep2=" be ", #elems=`Typ`, #pl=`@plevel`);
	  ";"; try_th_exps(); <br;
	  apply[following-sibling::*[position()=$it_step][name()="Let"]](#fst="1");
       }
   }
 }}

tpl [Assume] 
{ 
  pkeyword(#str="assume ");  
  if [count(*)>1] { pkeyword(#str="that "); <br; }
  andlist(#elems=`*`); ";"; 
  try_th_exps(); <br; 
} 

// should handle both the new version with the existential statement
// at the first position, and also the old version without it
tpl [Given] 
{ 
  $j=`@nr - 1`; 
  pkeyword(#str="given "); 
  jtlist(#j=$j, #sep2=" being ", #elems=`Typ`, #pl=`@plevel`); 
  pkeyword(#str=" such that ");
  andlist(#elems=`*[(name()="Proposition") and (position() > 1)]`); ";"; 
  try_th_exps(); <br; 
}

tpl [Take] { pkeyword(#str="take "); apply; ";"; try_th_exps(); <br; }
tpl [TakeAsVar] 
{ 
   pkeyword(#str="take "); 
   if [$const_links>0] 
   {   
      $addpl = { addp(#pl=`@plevel`); } 
      <a { @NAME=`concat("c",@nr,$addpl)`; }
   }
   ppconst(#nr=`@nr`, #vid = `Typ[1]/@vid`); " = ";   
   apply[*[2]]; 
   ";"; try_th_exps(); <br; 
}

tpl [Conclusion] 
{ 
   if [(By[@linked = "true"]) or 
       (IterEquality/IterStep[1]/By[@linked = "true"])] 
   { 
      pkeyword(#str="hence "); 
      apply[*[not(name() = "By")]]; 
      apply[By](#nbr = "1"); 
      try_th_exps(); 
      <br; 
   }
   else 
   { 
      if [Now] 
      {  
         <div 
	 { 
	    pkeyword(#str="hereby "); 
	    try_th_exps();
	    apply(#nkw = "1");  
	    pkeyword(#str="end;"); 
	 } 
      }
      else 
      { 
         pkeyword(#str="thus "); 

	 if [Proof] 
	 { 
	    apply[Proposition]; 
	    try_th_exps();
	    apply[Proof]; 
	 }
	 else 
	 { 
	    apply[Proposition]; 
	    apply[ IterEquality|By|From|ErrorInf|SkippedProof](#nbr = "1");
	    try_th_exps(); 
	    <br; 
	 } 
      } 
   }
}
// Auxiliary items

// First comes the reconstructed existential statement 
// and its justification, then the new local constants
// and zero or more propositions about them.
// For easier presentation, nr optionally contains the number   
// of the first local constant created here.      
//
//  element Consider { 
//    attribute nr { xsd:integer }?,
//    Proposition, Justification,
//    Typ+, Proposition*
//  }
tpl [Consider] 
{ 
   $j=`@nr - 1`; 

    
    if [By[@linked="true"]] { pkeyword(#str="then "); }

    pkeyword(#str="consider ");

   jtlist(#j = $j, #sep2 = " being ", #elems = `Typ`, #pl=`@plevel`);

   if [count(Proposition) > 1] 
   { 
      pkeyword(#str=" such that "); 
      <br; 
      andlist(#elems = `Proposition[position() > 1]`); 
   } 

   apply[*[2]]; 
}

// First comes the series of target types and reconsidered terms.
// For all these terms a new local variable with its target type
// is created, and its equality to the corresponding term is remembered.
// Finally the proposition about the typing is given and justified.
// For easier presentation, atNr optionally contains the number
// of the first local constant created here.
// Each type may optionally have presentational info about
// the variable (atVid) inside.
//  element elReconsider {
//    attribute atNr { xsd:integer }?,
//    (elTyp, Term)+,
//    elProposition, Justification
//  }
tpl [Reconsider] 
{ 
   $j=`@nr`; 
   if [By[@linked="true"]] { pkeyword(#str="then "); } 
   pkeyword(#str="reconsider ");
   $addpl = { if [$const_links>0] { addp(#pl=`@plevel`); } }
// should work both for old and new reconsider
    for-each [*[(not(name() = "Typ")) and (position() < (last() - 1))]] {
	 $p1  = `position()`;
	 $nr1 = `$j + $p1 - 1`;
	 if [$const_links>0] {<a { @NAME=`concat("c",$nr1,$addpl)`; }}
	 ppconst(#nr = $nr1, #vid = `../Typ[$p1]/@vid`);
	 " = ";
	 apply[.];
	 if [not($p1=last())] { ", "; }}

//  ppconst(#nr=$j, #vid = `Typ[1]/@vid`); " = "; 
//  jlist(#j=$j, #sep2=" = ", #elems=`*[(not(name() = "Typ")) 
//                        and (position() < (last() - 1))]`);
    " as "; apply[*[1]]; " "; 
    apply[*[last()]]; } 

tpl [Set] 
{ 
   pkeyword(#str="set "); 
   if [$const_links>0] 
   {   
      $addpl = { addp(#pl=`@plevel`); } 
      <a { @NAME=`concat("c",@nr,$addpl)`; }
   }
   ppconst(#nr=`@nr`, #vid=`Typ/@vid`); " = "; apply[*[1]]; ";"; <br; 
}

tpl [DefFunc] { pkeyword(#str="deffunc "); ppfunc(#nr=`@nr`); "(";  
                list(#separ=",", #elems=`ArgTypes/Typ`); ") "; pkeyword(#str="-> ");
                apply[*[3]]; " = ";
	        apply[*[2]]; ";"; <br; }
tpl [DefPred] { pkeyword(#str="defpred "); pppred(#nr=`@nr`); "["; 
                list(#separ=",", #elems=`ArgTypes/Typ`); "] "; pkeyword(#str="means ");
	        apply[*[2]]; ";"; <br; }

// Thesis after skeleton item, with definiens numbers
// forbid as default
tpl [Thesis] { }

tpl do_thesis(#nd)
{
  apply[ThesisExpansions];
  
  if [($display_thesis = 1) and (not($nd = 1))] 
  {
        " ";
        <a 
	{   
	  add_hs_attrs();
	  pcomment0(#str=" thesis: ");      
	}

	<span { @class="hide"; " "; apply[*[1]]; }
  }
}

tpl try_th_exps_old
  { 
     apply[./following-sibling::*[1][name()="Thesis"]/ThesisExpansions]; 
  }

// #nd overrides the $display_thesis parameter in do_thesis,
// used to supress the incorrect PerCases thesis now
tpl try_th_exps(#nd)
{ 
  if [./following-sibling::*[1][name()="Thesis"]]
  {  
    for-each [./following-sibling::*[1][name()="Thesis"]]
    {
      do_thesis(#nd=$nd); 
    }
  }
  else { if [((name(..) = "Now") or (name(..) = "CaseBlock") or (name(..) = "SupposeBlock"))
              and (../BlockThesis/Thesis)]
  {
    $prev_thesis_changes 
      = `count(./preceding-sibling::*[(name()="Let") or (name()="Take") 
	                               or (name()="TakeAsVar") or (name()="Assume")
	                               or (name()="Case") or (name()="Suppose")
				       or (name()="Given") or (name()="Conclusion")])`;
    for-each [ ../BlockThesis/Thesis[$prev_thesis_changes + 1]]
    {
      do_thesis(#nd=$nd);
    }
  }}
}

tpl [ThesisExpansions] { if [Pair] {
    " "; pcomment0(#str="according to "); 
    list(#separ=",", #elems=`Pair[@x]`); } }


tpl [ThesisExpansions/Pair] 
{
  $x       = `@x`;
  $doc     = { if [key('DF',$x)] { ""; } else { $dfs; } }

  $current = { if [$doc=""] { "1"; } else { "0"; } }

  for-each [document($doc,/)] 
  {
     for-each [key('DF',$x)] 
     {
        mkref(#aid = `@aid`, #nr = `@defnr`, #k = "D", #c = $current);
     }
  }
}



//  special block skeleton items 
//  element Suppose { Proposition+ }
//  element Case { Proposition+ }
tpl [Case|Suppose] 
{
  if [count(*)>1] 
  {
    pkeyword(#str="that ");
  }
   
  andlist(#elems = `*`); ";"; 
  // this will break the thesis display in diffuse statements 
  // for earlier kernel (analyzer v. < 1.94) - mea culpa, 
  // the only reasonable backward-compatibility fix would be to 
  // keep the kernel version as a parameter and check it here
  try_th_exps();
  <br;
}

// element PerCases { Proposition, Inference } 
tpl [PerCases] 
{
  <a 
  {
     add_hs_attrs();
     pkeyword(#str="cases ");
  }

  <span 
  {
    @class = "hide";
    apply [*[1]];
  }

  apply [*[position()>1]];

  // thesis after per cases is broken yet and would have 
  // to be reconstructed from subblocks' theses;
  // don't display it, only display the expansions
  try_th_exps(#nd="1");
}


//
// File: block_top.xsltxt - html-ization of Mizar XML, code for bloc and top elements
//
// Author: Josef Urban
//
// License: GPL (GNU GENERAL PUBLIC LICENSE)

// Registrations
tpl [RCluster] { 
    if [Presentation/RCluster] { apply [Presentation/RCluster]; }
    else {
       $nr1 = `@nr`;
       if [$generate_items>0]	{ 
// <xsl:document href="proofhtml/exreg/{$anamelc}.{$nr1}" format="html">
          rc();
// </xsl:document>
          $bogus=`1`;
       } 
       else {  <div { @about=`concat("#RC",$nr1)`; @typeof="oo:Theorem"; rc(); } }
    }
}

tpl rc 
{
  if [($mml="1") or ($generate_items>0)] { apply[ArgTypes]; }
  $nr1 = `@nr`;
  <a 
  { 
    @NAME=`concat("RC",$nr1)`;
    pkeyword(#str="cluster "); 
  }
  if [ErrorCluster] { "errorcluster"; } else { apply[*[3]](#all="1"); if[$regs_use_for=1] { " for"; } " "; apply[*[2]]; }
  ";"; <br; if [$mml="1"] { <br; }
}

tpl [CCluster] { 
    if [Presentation/CCluster] { apply [Presentation/CCluster]; }
    else {
      $nr1 = `@nr`;
      if [$generate_items>0]	{ 
// <xsl:document href="proofhtml/condreg/{$anamelc}.{$nr1}" format="html">
         cc();
// </xsl:document>
         $bogus=`1`;
      } 
      else {  <div { @about=`concat("#CC",$nr1)`; @typeof="oo:Theorem"; cc(); } }
    }
}


tpl cc
{ 
  if [($mml="1") or ($generate_items>0)] 
  { 
     apply[ArgTypes]; 
  }
  
  $nr1 = `@nr`;
  <a { 
       @NAME=`concat("CC",$nr1)`;
       pkeyword(#str="cluster "); }
       if [ErrorCluster] { "errorcluster"; }
       else 
       { 
          apply[*[2]](#all="1"); 
	  pkeyword(#str=" -> "); 
	  apply[*[4]]; 
	  if[$regs_use_for=1] { " for"; } " "; 
	  apply[*[3]]; 
       }
       ";"; <br; 
       if [$mml="1"] { <br; }
}

tpl [FCluster] { 
    if [Presentation/FCluster] { apply [Presentation/FCluster]; }
    else
    { 
      $nr1 = `@nr`;
      if [$generate_items>0]	{ 
// <xsl:document href="proofhtml/funcreg/{$anamelc}.{$nr1}" format="html">
       fc();
// </xsl:document>
       $bogus=`1`;
      } 
      else {  <div { @about=`concat("#FC",$nr1)`; @typeof="oo:Theorem"; fc(); } }
    }
}

tpl fc
{ 
   if [($mml="1") or ($generate_items>0)] { apply[ArgTypes]; }
   $nr1 = `@nr`;
   <a { @NAME=`concat("FC",$nr1)`;
   pkeyword(#str="cluster "); }
   if [ErrorCluster] { "errorcluster"; }
   else { apply[*[2]]; pkeyword(#str=" -> "); apply[*[3]]; if[Typ] { if[$regs_use_for=1] { " for"; } apply[Typ]; }}
   ";"; <br; if [$mml="1"] { <br; }
}


tpl [IdentifyWithExp|Identify] 
{ 
    $iname = `name()`; // to deal with both versions
    $nr1 = `@nr`;
    if [$generate_items>0]	
    { 
// <xsl:document href="proofhtml/idreg/{$anamelc}.{$nr1}" format="html">
       iy();
// </xsl:document>
   $bogus=`1`;
    } 
    else {  <div { @about=`concat("#IE",$nr1)`; @typeof="oo:Theorem"; iy(); } }
}

tpl iy
{ 
   $iname = `name()`; // to deal with both versions
   if [($mml="1") or ($generate_items>0)] 
   { 
      argtypes(#el=`Typ`);
   }

   $nr1 = `@nr`;

   <a 
   { 
      @NAME=`concat("IY",$nr1)`;
      pkeyword(#str="identify "); 
   }

   if [ErrorIdentify] { "erroridentify"; }
   else { if [($mml="1") or ($generate_items>0)] 
   { 
       if [$iname = 'Identify']
       {
           apply[Func[1]];
	   pkeyword(#str=" with "); 
	   apply[Func[2]];
       }
       else
       {
	   apply[*[position() = last() - 1]]; 
       	   pkeyword(#str=" with "); 
       	   apply[*[position() = last()]]; 
       }
   }
   else // try nice display from the compatibility formula
   {
     for-each [following-sibling::*[1]/Proposition/*[1]]
     {
       if [name() = "Pred"] // equality - terms
       { 
         apply[*[1]]; 
	 pkeyword(#str=" with "); 
	 apply[*[2]];
       }
       else { if [name() = "And"] // equivalence - predicates
       {
         $e1= is_equiv(#el=`.`);
	 if [$e1="1"] 
	 { 
	   apply[*[1]/*[1]/*[1]]; 
	   pkeyword(#str=" with ");
	   apply[*[1]/*[1]/*[2]/*[1]];
	 }
	 else 
	 {
	   "IDENTIFY DISPLAY FAILED -  PLEASE COMPLAIN!"; <br;
	   apply[.];		 
	 }
       }
       else 
       {
         $i3= is_impl1(#el=`.`);
	 if [not($i3=2)] { "IDENTIFY DISPLAY FAILED -  PLEASE COMPLAIN!";  }
	 else
	 {
           for-each [*[1]/*[@pid=$pid_Impl_RightNot]/*[1]]
	   {
	     if [name() = "Pred"] 
	     {
	       apply[*[1]]; 
	       pkeyword(#str=" with "); 
	       apply[*[2]];
	     }
	     else 
	     {
	       $e1= is_equiv(#el=`.`);
	       if [$e1="1"] 
	       { 
	         apply[*[1]/*[1]/*[1]]; 
		 pkeyword(#str=" with ");
		 apply[*[1]/*[1]/*[2]/*[1]];
               }
	       else 
	       {
	         "IDENTIFY DISPLAY FAILED -  PLEASE COMPLAIN!"; <br;
		 apply[.];		 
	       }
	     }
	   }
	   pkeyword(#str=" when ");
	   ilist(#separ = ", ", #elems=`*[1]/*[not(@pid=$pid_Impl_RightNot)]`); 
	 }
       }}
     }
   }}

   ";"; <br; if [$mml="1"] { <br; }
}

tpl [Reduction] 
{ 
    $nr1 = `@nr`;
    if [$generate_items>0]	
    { 
// <xsl:document href="proofhtml/redreg/{$anamelc}.{$nr1}" format="html">
       reduce();
// </xsl:document>
   $bogus=`1`;
    } 
    else {  <div { @about=`concat("#RD",$nr1)`; @typeof="oo:Theorem"; reduce(); } }
}

tpl reduce
{ 
   if [($mml="1") or ($generate_items>0)] 
   { 
      argtypes(#el=`Typ`);
   }

   $nr1 = `@nr`;

   <a 
   { 
      @NAME=`concat("RD",$nr1)`;
      pkeyword(#str="reduce "); 
   }

   if [ErrorReduction] { "errorreduction"; }
   else { if [($mml="1") or ($generate_items>0)] 
   { 
	   apply[*[position() = last() - 1]]; 
       	   pkeyword(#str=" to "); 
       	   apply[*[position() = last()]]; 
   }
   else // try nice display from the compatibility formula
   {
     for-each [following-sibling::*[1]/Proposition/*[1]]
     {
       if [name() = "Pred"] // equality - terms
       { 
         apply[*[1]]; 
	 pkeyword(#str=" to "); 
	 apply[*[2]];
       }
       else 
       {
          "REDUCE DISPLAY FAILED -  PLEASE COMPLAIN!"; <br;
	  apply[.];		 
       }
     }
   }}
   ";"; <br; if [$mml="1"] { <br; }
}




// ignore them
tpl [Reservation/Typ] { ""; }
tpl [Definiens/*] { ""; }


tpl add_comments(#line)
{
  if[$mk_comments > 0] 
  { 
    $prevline = `$line - 1`;
    for-each [document($cmt,/)]
    {
       for-each [key('CMT',$prevline)]
       {
         apply[.];
       } 
    }
    $prevline1 = `$line - 2`;
    for-each [document($cmt,/)]
    {
       for-each [key('CMT',$prevline1)]
       {
         apply[.];
       } 
    }
  }
}

// http://en.wikipedia.org/wiki/Cantor_Theorem to
// http://dbpedia.org/resource/Cantor_theorem
tpl wp2dp(#txt)
{
   `concat("http://dbpedia.org/resource/",substring-after($txt,'/wiki/'))`;
}

tpl add_dbpedia(#line)
{
  if[$mk_comments > 0] 
  { 
    $prevline = `$line - 1`;
    for-each [document($cmt,/)]
    {
       for-each [key('CMT',$prevline)]
       {
          for-each [CmtLink/a]
	  {
	     $dbplink = wp2dp(#txt=`@href`); 
	     <span { @rel="owl:sameAs"; @resource=$dbplink; }
	  }
       } 
    }
  }
}


// xsltxt cannot use xsl:document yet, so manually insert it 
// (now done by the perl postproc)
// the bogus is there to ensure that the ending xsl:doc element
// is printed by xslxtxt.jar too
tpl [JustifiedTheorem] 
{
    add_comments(#line=`@line`);
    $nr1 = `1+count(preceding-sibling::JustifiedTheorem)`;
    if [$generate_items>0]	
    { 
// <xsl:document href="proofhtml/th/{$anamelc}.{$nr1}" format="html">
       jt();
// </xsl:document>
       $bogus=`1`;
    } 
    else 
    { 
      // optional interestingness rating produced by external soft
      if [@interesting > 0]
      {
         // scale red and blue from 0% (green) to 100% (white)
         $intensity = `(1 - @interesting) * 100`;
         <div 
	 { 
            @about=`concat("#T",$nr1)`; @typeof="oo:Theorem";
	    add_dbpedia(#line=`@line`);
	    @style=`concat("background-color:rgb(",$intensity,"%,100%,", $intensity, "%);")`;
	    jt();
         }
      }
      else { <div { @about=`concat("#T",$nr1)`; @typeof="oo:Theorem"; add_dbpedia(#line=`@line`); jt();} }
    }
    if [$mk_ajax_refs>0]
    { 
// <xsl:document href="{$ajax_refs_dir}/{$anamelc}/T{$nr1}" format="html">
	<div { jt(#noproof="1"); }
// </xsl:document>
        $bogus=`1`;
    }
}

// private - assumes that is inside JustifiedTheorem
tpl jt(#noproof) 
{
    $nr1 = `1+count(preceding-sibling::JustifiedTheorem)`;

    thm_header(#nr1=$nr1);

    if [Proof] 
    { 
       <div { @class="add"; apply[*[1]/*[1]]; } 
       if [(not($noproof="1")) and (not($generate_items>0) or ($generate_items_proofs>0))]
       {
         apply[*[2]]; 
       }
    }
    else 
    { 
       <div 
       { 
          @class="add"; 

          if [Proposition/Verum] 
	  { 
	     pkeyword(#str="canceled; ");
	  }
	  else 
	  { 
	     apply[*[1]/*[1]]; " "; 
	     apply[*[2]]; 
	  } 
       } 
    } 
}


// private inside jt
tpl thm_header(#nr1)
{
    pkeyword(#str="theorem "); 

    if [($proof_links > 0) and ($print_lab_identifiers = 0)]
    { 
       plab1(#nr=$nr1,#txt="Th"); ": "; 
    }
    else 
    { 
       for-each [Proposition[@nr > 0]] { pplab(#nr=`@nr`, #vid=`@vid`); ": "; }
    }

    <a 
    { 
       @NAME = `concat("T", $nr1)`; 
       pcomment0(#str = `concat($aname,":", $nr1)`); 
       if [@interesting > 0] 
       { 
          " interestingness: "; `@interesting`;
       }
       if [$idv > 0] 
       { 
          idv_for_item(#k="t", #nr=$nr1);
       }
       if [$wiki_sections = 1]
       {
         $endpos = { if [Proof] { `Proof[1]/EndPosition[1]/@line`; }
                     else { if [By|From]  { `*[2]/@line`; } 
		     else { "0"; } }}  

         if [$endpos > 0]
	 {
           " "; wiki_edit_section_for(#k="t", #nr=$nr1, #line1=`Proposition[1]/@line`, #line2=$endpos);
         }

       }      
       if [$thms_tptp_links = 1]
       {
          tptp_for_thm(#line=`Proposition[1]/@line`, #col=`Proposition[1]/@col`);
	  " "; add_ar_iconif(#line=`Proposition[1]/@line`, #col=`Proposition[1]/@col`); 
	  " "; edit_for_thm(#line=`Proposition[1]/@line`, #col=`Proposition[1]/@col`);
       }

       <br;
    }
}


tpl idv_for_item(#k,#nr)
{
  $idv_html = "http://www.cs.miami.edu/~tptp/MizarTPTP/";
// "http://lipa.ms.mff.cuni.cz/~urban/idvtest/";

//  $idv_html = "file:///home/urban/mptp0.2/idvhtml/";
  $tptp_file = `concat($idv_html,"problems/",$anamelc,"/",$anamelc, "__",$k, $nr, "_", $anamelc)`;
  " ";
  <img 
  {
    add_hs2_attrs();
    @src="PalmTree.jpg";
    @title="Show IDV graph";
    @alt="Show IDV graph";
  }

//   <a 
//   { 
// //    add_ajax_attrs(#u = $th);
//     add_hs2_attrs();
//     @title="Show IDV graph";
//     <b { " IDV graph "; } 
//   }

  <span 
  { 
      @style = "display:none"; 
      ":: Showing IDV graph ... (Click the Palm Tree again to close it)"; 
      <APPLET 
      { 
         @CODE = "IDVApplet.class";
	 @ARCHIVE = "http://www.cs.miami.edu/students/strac/test/IDV/IDV.jar,http://www.cs.miami.edu/students/strac/test/IDV/TptpParser.jar,http://www.cs.miami.edu/students/strac/test/IDV/antlr-2.7.5.jar";
	 @WIDTH = "0";
	 @HEIGHT = "0";
	 <PARAM { @NAME="URL"; @VALUE=$tptp_file; }
      }
  }
}


tpl tptp_for_thm(#line, #col)
{
  $tptp_file = `concat("problems/",$anamelc,"/",$anamelc,"__",$line,"_",$col)`;
  " ::";
  <a
  {
    @href= `concat($ltmpftptpcgi,"?file=",$tptp_file,"&tmp=",$lbytmpdir)`; 
    @target= `concat("MizarTPTP",$lbytmpdir)`;
    <img
    {
       @src= `concat($ltptproot,"TPTP.gif")`;
       @height= "17";
       @width= "17";
       @alt= "Show TPTP problem";
       @title= "Show TPTP problem";
    }
  }
} 

tpl add_ar_iconif(#line,#col) 
{ 
   if [$linkarproofs>0] 
   { 
      $byurl = 
      { 
         choose 
	 { 
	    when [$linkby=1] { `concat($lbydir,$anamelc,"/",$line,"_",$col,".html")`; }
	    when [$linkby=2] { `concat($lbydlicgipref,$anamelc,"/",$line,"_",$col,".dli")`; } 
	    when [$linkby=3] { `concat($lbytptpcgi,"?article=",$anamelc,"&lc=",$line,"_",$col,"&tmp=",$lbytmpdir,$lbycgiparams)`; } 

	 } 
      }

      <a { 
            if[$ajax_by > 0] { add_ajax_attrs(#u=$byurl); }
	    else
	    {
	       @href=$byurl; @class="txt"; 
	       if[$linkbytoself > 0] {@target="_self"; } else {@target="byATP";} 
            }
	    $txt = { mk_by_title(#line=$line,#col=$col); }
	    if [$by_titles>0] { @title=mk_by_title(#line=$line,#col=$col); }
	    <img
	    {
       	       @src= `concat($ltptproot,"AR.gif")`;
       	       @alt= $txt;
	       if [$by_titles>0] { @title = $txt; }
            }
	    " ";  
	 }
      if[$ajax_by > 0] { <span { " "; } } 
    }
}


tpl edit_for_thm(#line, #col)
{
//  $tptp_file = `concat($anamelc,".miz")`;
  $thm_file = `concat($anamelc,"__",$line,"_",$col)`;
  " ::";
  <a
  {
//    @href= `concat($ltmpftptpcgi,"?file=",$tptp_file,"&tmp=",$lbytmpdir,"&pos=",$line)`; 
    @href= `concat($ltmpftptpcgi,"?file=",$thm_file,"&tmp=",$lbytmpdir)`; 
    "[edit]";
  }
}

tpl wiki_edit_section_for(#k, #nr, #line1, #line2)
{
  $section = `concat($k,$nr,"_",$line1,"_",$line2)`;
// // <xsl:document href="{$anamelc}__{$k}{$nr}.itm">
//  $bogus=`1`;
//  $section;
// // </xsl:document>
  <a
  {
    @href= `concat($lmwikicgi,"?p=",$lgitproject,";a=edit;f=mml/",$anamelc,".miz;s=",$section)`; 
    @rel="nofollow";
    @class="edit";
    " [edit]";
  }
}



tpl [DefTheorem] 
{ 
    $nr1 = `1+count(preceding-sibling::DefTheorem)`;
    if [$generate_items>0]	
    { 
// <xsl:document href="proofhtml/def/{$anamelc}.{$nr1}" format="html">
       dt(#nohide="1");
// </xsl:document>
       $bogus=`1`;
    } 
    else {  <div { @about=`concat("#DT",$nr1)`; @typeof="oo:Definition"; dt(); } }

    if [$mk_ajax_refs>0]
    { 
// <xsl:document href="{$ajax_refs_dir}/{$anamelc}/D{$nr1}" format="html">
	<div { dt(#nohide="1"); }
// </xsl:document>
   $bogus=`1`;
    }
}

// private - assumes that is inside DefTheorem
tpl dt(#nohide)
{
  $nr1 = `1+count(preceding-sibling::DefTheorem)`;

  ":: "; pkeyword(#str="deftheorem ");

  if [($proof_links > 0) and ($print_lab_identifiers = 0)]
  { 
     plab1(#nr = $nr1, #txt = "Def"); 
  } 
  else 
  { 
     for-each [Proposition[@nr > 0]] { pplab(#nr = `@nr`, #vid = `@vid`); }
  } 

  " ";
  //    <a { @NAME=`concat("D",$nr1)`; 
  if [@constrkind] 
  { 
     "  defines "; 
     abs(#k = `@constrkind`, #nr = `@constrnr`, 
         #sym = abs1(#k = `@constrkind`, #nr = `@constrnr`)); 
  } 

  " ";
  <a 
  { 
     @onclick = "hs(this)"; 
     @href    = "javascript:()";
     `concat($aname, ":def ", $nr1)`; 
     " : "; <br; 
  }

  <span 
  { 
     if [not($nohide="1")] { @class = "hide"; }

// ##NOTE: div is not allowed inside span
//     <div 
//     {   
//        @class = "add"; 

	if [Proposition/Verum] 
	{ 
	   pkeyword(#str="canceled; "); 
        }
	else 
	{ 
	   apply[*[1]/*[1]];  ";"; 
	}  
//     }
       <br; 
  }
}

//   Property, elProposition, Justification
tpl [JustifiedProperty] 
{
   $nm = { lc(#s = `name(*[1])`); }

   <a 
   { 
      add_hs_attrs(); 
      if [$nm = "antisymmetry"] { pkeyword(#str="asymmetry"); } 
      else { pkeyword(#str=$nm); } " "; 
     
   }

   <span { @class="hide"; <br; apply[*[2]]; }
   apply[*[position()>2]]; 
}

//  Formula | ( elProposition, Justification )
tpl [UnknownCorrCond|Coherence|Compatibility|Consistency|Existence|Reducibility|Uniqueness] 
{ 
   <a 
   { 
      add_hs_attrs();
      $nm = { lc(#s = `name()`); }
      pkeyword(#str=$nm); " ";
   }

   <span { @class="hide"; <br; apply[*[1]]; }
   if [count(*)>1] { apply[*[position()>1]];  } else { ";"; <br; }
}

// CorrectnessCondition*, elProposition, Justification
tpl [Correctness] { 
<a { add_hs_attrs(); pkeyword(#str="correctness "); }
// apply to subconditions , skip their conjunction
<span { @class="hide"; <br; apply[*[position()<(last()-1)]]; }
apply[*[position()=last()]]; }

tpl [Canceled] { pkeyword(#str="canceled;"); <br; }

tpl [SchemeFuncDecl] { 
     pschfvar(#nr=`@nr`); "(";
     list(#separ=",", #elems=`ArgTypes/Typ`); ") "; pkeyword(#str="-> ");
     apply[*[2]]; }

tpl [SchemePredDecl] { 
     pschpvar(#nr=`@nr`); "[";
     list(#separ=",", #elems=`ArgTypes/Typ`); "]"; }

//   ( elSchemeFuncDecl | elSchemePredDecl )*,
//   element elSchemePremises { elProposition* },
//   elProposition, Justification, elEndPosition
tpl [SchemeBlock] 
{
    add_comments(#line=`@line`);
    if [$generate_items>0]	
    { 
// <xsl:document href="proofhtml/sch/{$anamelc}.{@schemenr}" format="html">
       sd();
// </xsl:document>
   $bogus=`1`;
   } 
   else {  <div { @about=`concat("#S",@schemenr)`; @typeof="oo:Theorem"; add_dbpedia(#line=`@line`); sd(); } } 

    if [$mk_ajax_refs>0]
    { 
// <xsl:document href="{$ajax_refs_dir}/{$anamelc}/S{@schemenr}" format="html">
	<div { sd(#noproof="1"); }
// </xsl:document>
        $bogus=`1`;
    }
}

tpl sd(#noproof)
{
  <div 
  { 
    <a 
    { 
      @NAME=`concat("S",@schemenr)`; pkeyword(#str="scheme  ");
      pcomment(#str=`concat($aname,":sch ",@schemenr)`); 
    }
//     "s"; `@schemenr`; 

    if [($proof_links > 0) and ($print_lab_identifiers = 0)]
    { 
       plab1(#nr = `@schemenr`, #txt = "Sch"); 
    } 
    else 
    { 
       pplab(#nr = `@schemenr`, #vid = `@vid`, #txt = "Sch");
    }

    "{ ";
    list(#separ=", ", #elems=`SchemeFuncDecl|SchemePredDecl`); 
    " } :"; <br;
    <div { @class="add"; apply[Proposition]; } 
    if [SchemePremises/Proposition] 
    { 
       pkeyword(#str="provided");
       <div 
       { 
          @class="add"; 
	  andlist(#elems=`SchemePremises/Proposition`); 
       } 
    }
    if [(not($noproof="1")) and (not($generate_items>0))]
    {
       apply[*[position() = last() - 1]];
    }
  }
}


//   ( ( CorrectnessCondition*, elCorrectness?,
//       elJustifiedProperty*, elConstructor?, elPattern? )
//   | ( elConstructor, elConstructor, elConstructor+,
//       elRegistration, CorrectnessCondition*, 
//       elCorrectness?, elPattern+ ))
// ##TODO: commented registration and strict attr for defstruct
tpl [Definition] 
{    
    add_comments(#line=`@line`); 
    if [@expandable = "true"] 
    { 
       $argtypes = `../Let/Typ`;
       $loci = { if [($mml="1") or ($generate_items>0)] { "1"; } else { "2"; }}
       for-each [Pattern] 
       {
          <a 
	  { 
	     @NAME=`concat("NM", @nr)`;
	     pkeyword(#str="mode ");  
	     abs1(#k = "M", #fnr = `@formatnr`);

	     if [Visible/Int] 
	     { 
	        " of "; 

		for-each [Visible/Int] 
		{ 

		   $x=`@x`;

		   if [$loci="2"] 
		   { 
		      ppconst(#nr= $x,#vid=`$argtypes[position()=$x]/@vid`); 
                   } 
		   else { ploci(#nr=$x); }

		   if [not(position()=last())] { ","; } 
                }
             }

	     pkeyword(#str=" is "); 
          }
 
	  apply[Expansion/Typ]; ";"; 
	  <br; 
       }
    }
    else 
    { 
       // @nr is present iff Definiens is present; it can be 0 if
       // the definiens is not labeled, otherwise it is the proposition number
       // of its deftheorem
       if [@nr and ($generate_items>0)]	
       { 
          $cnt1 = `1 + count(preceding-sibling::Definition[@nr])`;
	  $defnr = `../following-sibling::Definiens[position() = $cnt1]/@defnr`;
// <xsl:document href="proofhtml/dfs/{$anamelc}.{$defnr}" format="html">
          dfs();
// </xsl:document>
          $bogus = `1`;
       }
       else 
       {
          if [@nr]
	  {
	     <div { @about=`concat("#D",@nr)`; @typeof="oo:Definition"; add_dbpedia(#line=`@line`); dfs(); }
	  }
	  else
       	  {  
             dfs(); 
       	  }
       }
    }

    apply[*[not((name()='Constructor') or (name()='Pattern') 
                or (name()='Registration'))]]; 
}

tpl dfs() 
{
    $nl = { if [@nr] { "0"; } else { "1"; }}
    $argtypes = `../Let/Typ`;
// Constructor may be missing, if this is a redefinition
// that does not change its types. In that case, the Constructor needs
// to be retrieved from the Definiens - see below.

    if [not(@nr)] 
    { 
        // for generate_items, we have to take loci from the constructor here
       $indef1 = { if [($generate_items > 0)] { "0"; } else { "1"; } }

       apply[Constructor](#indef = $indef1, #nl = $nl, #argt = $argtypes);
    } 

// @nr is present iff Definiens is present; it can be 0 if
// the deiniens is not labeled, otherwise it is the proposition number
// of its deftheorem
    if [@nr] 
    {  
       $nr1   = `@nr`;
       $vid   = `@vid`;
       $cnt1  = `1 + count(preceding-sibling::Definition[@nr])`;
       $cnstr = `count(Constructor)`;

       if [($generate_items > 0)]  
       { 
	  // Definiens is better than Constructor for loci display,
	  // since Constructor may be missing for redefinitions.
          for-each [../following-sibling::Definiens[position() = $cnt1]] 
	  {
	     argtypes(#el=`Typ`);
          }
       }

       apply[Constructor](#indef = "1", #nl = $nl, #argt = $argtypes);

       for-each [../following-sibling::Definiens[position() = $cnt1]] 
       {
          $ckind = `@constrkind`; 
	  $cnr   = `@constrnr`;

	  if [$cnstr = 0] 
	  {
             // here the redefined constructor is retrieved from definiens 
	     pkeyword(#str="redefine ");

	     $doc = { if [key($ckind, $cnr)] { ""; } else { $constrs; } }

	     for-each [document($doc, /)] 
	     { 
	        apply[key($ckind, $cnr)](#indef = "1", #nl = $nl, #argt = $argtypes, #nrt= "1",#old="1"); 
	     } 
          }

	  if [DefMeaning/@kind = 'e'] { pkeyword(#str=" equals "); } 
	  else { pkeyword(#str=" means "); }

	  if [$nr1 > 0]  
	  { 
	     ":"; 

	     if [($proof_links > 0) and ($print_lab_identifiers = 0)]
	     { 
	        plab1(#nr = `@defnr`, #txt = "Def");
	     } 
	     else 
	     { 
	        pplab(#nr = $nr1, #vid = $vid); 
	     }

	     ": ";
	  }

	  <a 
	  { 
	     @NAME = `concat("D", @defnr)`; 
	     pcomment(#str = `concat($aname, ":def ", @defnr)`); 
	  }

         // note that loci below can be translated to constants and identifiers
         // - see definition of LocusVar
	 for-each [DefMeaning/PartialDef] 
	 { 
	    apply[*[1]]; 
	    pkeyword(#str=" if "); 
	    apply[*[2]]; 
	    <br; 
	 }

	 if [(DefMeaning/PartialDef) 
	    and (DefMeaning/*[(position() = last()) 
		and not(name()="PartialDef")])] 
         { 
	    pkeyword(#str=" otherwise ");
	 }

	 apply[DefMeaning/*[(position() = last()) and not(name()="PartialDef")]]; 

         ";"; <br;
      }
   } 
}



//   ( elLet | elAssume | elGiven | AuxiliaryItem |
//     elCanceled | elDefinition )*, elEndPosition
tpl [DefinitionBlock] 
{
   add_comments(#line=`@line`);
   <div 
   { 
      pkeyword(#str="definition");
      <div { @class="add"; apply[*[not(name()='EndPosition')]]; }
      pkeyword(#str="end;");
   }
}

//   ( elRCluster | elFCluster | elCCluster ),
//   CorrectnessCondition*, elCorrectness?
tpl [Registration] { apply; }

//   elIdentifyWithExp, CorrectnessCondition*, elCorrectness?
tpl [IdentifyRegistration] { apply; }

tpl [ReductionRegistration] { apply; }

tpl [PropertyRegistration] { apply; }


//   ( elLet | AuxiliaryItem | elRegistration | elCanceled )+, elEndPosition
tpl [RegistrationBlock] 
{
    add_comments(#line=`@line`);
    <div { pkeyword(#str="registration");
    <div { @class="add"; apply[*[not(name()='EndPosition')]]; }
    pkeyword(#str="end;"); }  
} 

tpl [NotationBlock] 
{
    <div { pkeyword(#str="notation");
    <div { @class="add"; apply[*[not(name()='EndPosition')]]; }
    pkeyword(#str="end;"); }  
} 


// Blocks
tpl [BlockThesis] { } // "blockthesis: "; apply; ";"; <br; }

//   (  ( elBlockThesis, elCase, elThesis, Reasoning )
//   |  ( elCase, Reasoning, elBlockThesis ) )
tpl [CaseBlock] 
{ 
    <div { <a { add_hsNdiv_attrs(); if [$proof_links>0] { @title=`@newlevel`; } pkeyword(#str="case "); }
    apply[Case];
    <div { @class="add"; apply[*[not(name()='Case')]]; }
    pkeyword(#str="end;"); } 
}

tpl [SupposeBlock] 
{
    <div { <a { add_hsNdiv_attrs(); if [$proof_links>0] { @title=`@newlevel`; } pkeyword(#str="suppose "); } 
    apply[Suppose];
    <div { @class="add"; apply[*[not(name()='Suppose')]]; }
    pkeyword(#str="end;"); } 
}

//   (  ( elBlockThesis, ( elCaseBlock+ | elSupposeBlock+ ),
//        elPerCases, elThesis, elEndPosition  )
//   |  ( ( elCaseBlock+ | elSupposeBlock+ ),
//        elPerCases, elEndPosition, elBlockThesis ) )
tpl [PerCasesReasoning] 
{
    <div 
    { 
       <a 
       { 
          add_hsNdiv_attrs(); 
	  if [$proof_links>0] { @title=`@newlevel`; } 
	  pkeyword(#str="per "); 
       }

       apply[PerCases];

       <div 
       { 
          @class="add"; apply[BlockThesis];
	  apply[Thesis];
	  apply[CaseBlock | SupposeBlock]; 
       }

       pkeyword(#str="end;"); 
    } 
}

//   elBlockThesis, Reasoning 
// the Proof is done in two parts, as a preparation for printing
// top proofs into separate documents, and their loading via AJAX
// this is a non-top-level proof
tpl [Proof/Proof | Now/Proof | Conclusion/Proof | CaseBlock/Proof | SupposeBlock/Proof]
{
    <div 
    { 
       <a 
       { 
          add_hs2_attrs(); 
	  if [$proof_links>0] { @title=`@newlevel`; } 
	  pkeyword(#str="proof "); 
       }
//       add_ar_iconif(#line=`EndPosition[1]/@line`, #col=`EndPosition[1]/@col`);
       <div { @class="add"; apply; }
       pkeyword(#str="end;"); 
    } 
}

// hence the rest is a top-level proof
// xsltxt cannot use xsl:document yet, so manually insert
// (now done as perl postproc)
// if you want ajax_proofs
tpl [Proof] {
    $nm0 = `concat($ajax_proof_dir,"/",$anamelc,"/",@newlevel)`;
    $nm =  { if[$ajax_proofs=3] { `concat($ltmpftptpcgi,"?tmp=",$lbytmpdir,"&raw=1","&file=",$nm0)`; } else { $nm0; } }
    <div {
    	 @about=`concat("#PF",@newlevel)`; @typeof="oo:Proof"; 
	 choose 
	 {
	    when[(name(..) = "JustifiedTheorem")] { <span { @rel="oo:proves"; @resource=`concat("#T",../@nr)`; } }
	    when[(name(..) = "SchemeBlock")] { <span { @rel="oo:proves"; @resource=`concat("#S",../@schemenr)`; } }
	    // toplevel lemma, hopefully
	    when[not(string-length(@plevel)>0)] {  <span { @rel="oo:proves"; @resource=`concat("#E",preceding-sibling::Proposition[1]/@propnr)`; } }
	 }
	 <a { 
	    if [($ajax_proofs=1) or ($ajax_proofs=3)]	{ add_ajax_attrs(#u=$nm); } else { add_hs2_attrs(); }
	    if [$proof_links>0] { @title=`@newlevel`; } 
	    pkeyword(#str="proof "); 
	    }

 //	  add_ar_iconif(#line=`EndPosition[1]/@line`, #col=`EndPosition[1]/@col`); 
         if [$ajax_proofs>0]	{ <span { if[$ajax_proofs=2] {@filebasedproofinsert=`@newlevel`;}} 
// <xsl:document href="{$ajax_proof_dir}/{$anamelc}/{@newlevel}" format="html">
	    <div { @class="add"; apply; }
// </xsl:document>
   $bogus=`1`;
 }
	 else { <div { @class="add"; apply; } }
	 pkeyword(#str=$top_proof_end); 
	 } 
     }


//   Reasoning, elBlockThesis 
// #nkw tells not to print the keyword (used if hereby was printed above)
// ###TODO: fix for generating items (see Proposition)
tpl [Now](#nkw) 
{
    if [not($nkw="1")] 
    { 
       <div 
       { 
          if [@nr>0] { pplab(#nr=`@nr`, #vid=`@vid`); ": ";}

	  <a 
	  { 
	     add_hs2_attrs(); 
	     if [$proof_links>0] { @title=`@newlevel`; } 
	     pkeyword(#str="now "); 

	     if [($display_thesis = 1)] 
    	     {
      	       for-each [ BlockThesis]
  	       {
                  " ";   
               	  <a 
		  {   
	  	     add_hs_attrs();
	  	     pcomment0(#str=" thesis: ");      
		  }

		  <span { @class="hide"; " "; apply[*[position()=last()]]; }
  	       }
    	     }
          }

          now_body();

	  pkeyword(#str="end;"); 
       }
    }
    else {  now_body(); }
}


tpl now_body
{
   <div 
   { 
      @class="add"; 
      apply[BlockThesis];
      apply[*[not(name()='BlockThesis')]]; 
   } 
}


tpl idv_for_top()
{
  $idv_html = "http://lipa.ms.mff.cuni.cz/~urban/idvtest/";

//  $idv_html = "file:///home/urban/mptp0.2/idvhtml/";
  $tptp_file = `concat($idv_html,"top/",$anamelc,".top.rated")`;
  " ";
  <img 
  {
    add_hs2_attrs();
    @src="hammock.jpg";
    @title="Show IDV graph for whole article";
    @alt="Show IDV graph for whole article";
  }

//   <a 
//   { 
// //    add_ajax_attrs(#u = $th);
//     add_hs2_attrs();
//     @title="Show IDV graph";
//     <b { " IDV graph "; } 
//   }

  <span 
  { 
      @style = "display:none"; 
      ":: Showing IDV graph ... (Click the Palm Trees again to close it)"; 
      <APPLET 
      { 
         @CODE = "IDVApplet.class";
	 @ARCHIVE = "IDV.jar,TptpParser.jar,antlr-2.7.5.jar";
	 @WIDTH = "0";
	 @HEIGHT = "0";
	 <PARAM { @NAME="URL"; @VALUE=$tptp_file; }
      }
  }
}



// tpl [Now](#nkw) {
//     <div { <b { if [not($nkw="1")] { "now ";} }
//     <div { @class="add"; apply[BlockThesis];
//            apply[*[not(name()='BlockThesis')]]; } 
//     pkeyword(#str="end;"); } } 

// separate top-level items by additional newline
tpl [Article] 
{ 
  <div
  {
    if [not($mk_header > 0)]
    {
       pcomment0(#str=`concat($aname, "  semantic presentation")`); 
    }
    if [$idv > 0] 
    { 
       idv_for_top();
    }
  }
    <br;

    for-each [*] 
    { 
      apply[.]; 
      if [(not(name()='Definiens')) and (not(name()='Reservation'))] { <br;} 
    } 
}

tpl [Section] { pkeyword(#str="begin"); <br; }

// processing of imported documents
tpl [Theorem] 
{ 
   pkeyword(#str="theorem "); 
   mkref(#aid=`@aid`, #nr=`@nr`, #k=`@kind`); <br; 
   if [Verum] { pkeyword(#str="canceled; "); } else { apply; } 
   <br; <br; 
}

// now used only when #mml=1 - in article the block has them
tpl [ArgTypes] { argtypes(#el = `*`); }

tpl argtypes(#el)
{ 
   if [$el] 
   { 
      pkeyword(#str="let "); 
      ploci(#nr="1");
      " be "; 
      alist(#j="1", #sep1=", ", #sep2=" be ", #elems=`$el`); 
      ";"; <br; 
   }
}

// #indef tells not to use Argtypes (we are inside Definition)
// note that this can also be used for displaying 
// environmental constructors, or constructor retrieved from other file
// #argt is explicit list of argument types, useful for
// getting the @vid (identifier numbers) of loci
// #nrt tells not to show the result type(s)
// #old says that the constructor is from a redefinition and not new,
//      so an anchor should not be created
tpl [Constructor](#indef,#nl,#argt,#nrt,#old) 
{ 
    $loci = { if [($mml="1") or ($generate_items>0)] { "1"; } else { "2"; }}

    if [not($indef="1")] { apply[ArgTypes]; }

    if [@redefnr>0] 
    { 
       pcomment0(#str = "original: ");
       abs(#k=`@kind`,#nr=`@redefnr`,#sym=abs1(#k=`@kind`, #nr=`@redefnr`));
       <br;
       pkeyword(#str="redefine ");
    }

    $mk = { mkind(#kind=`@kind`); }

    if [$old="1"] { pkeyword(#str=$mk);  " "; }
    else
    {
       <a { @NAME=`concat(@kind,@nr)`; pkeyword(#str=$mk);  " "; }
    }
 
    if [@kind="G"] 
    { 
       abs(#k=`@kind`,#nr=`@relnr`,#sym=abs1(#k=`@kind`, #nr=`@relnr`)); 
       "(# "; 

       for-each [Fields/Field] 
       { 
          abs(#k="U",#nr=`@nr`,#sym=abs1(#k="U", #nr=`@nr`)); 
	  if [not(position()=last())] { ", "; } 
       }

       " #)"; 
    }
    else 
    { 
       if [@kind='V'] 
       {
          $nr1 = `count(ArgTypes/Typ)`;
          if [$loci = 1] { ploci(#nr = $nr1); }
	  else { ppconst(#nr = $nr1, #vid = `$argt[position() = $nr1]/@vid`); }
	  " is ";  
       	  pp(#k=`@kind`,#nr=`@relnr`, #args = `$argt[position() < last()]`, #loci=$loci);
	  // abs(#k=`@kind`, #nr=`@relnr`, #sym=abs1(#k=`@kind`, #nr=`@relnr`)); 
       }
       else { pp(#k=`@kind`,#nr=`@relnr`, #args = $argt, #loci=$loci); }
       // "( ";  arglist(#separ=",", #elems=`ArgTypes/Typ`); ")"; 
    }

    if [not($nrt = 1) and 
        ((@kind = 'M') or (@kind = 'K') or (@kind= 'G') 
         or (@kind= 'U') or (@kind= 'L'))] 
    { 
       pkeyword(#str=" -> ");
       // note that loci in Typs here can be translated to constants and identifiers
       // - see definition of LocusVar
       list(#separ=",",#elems=`Typ`); 
    }
 
    if [not($indef="1")]  
    {  
       ";"; <br;  <br; 
    }
    else { if [$nl="1"] { ";"; <br;} }
}

// display synonym and antonym definiiotns
tpl [NotationBlock/Pattern] 
{
// pp1(#k=`@constrkind`,#nr=`@constrnr`,#vis=`Visible/Int`,
// #fnr=`@formatnr`, #loci="1"); <br;
  $loci = { if [$mml="1"] { "1"; } else { "2"; }}
  $argtypes = `../Let/Typ`;
  <a { 
       @NAME=`concat("N",@kind,@nr)`;
       if [@antonymic] { pkeyword(#str="antonym "); } else { pkeyword(#str="synonym "); }
       pp1(#k=`@constrkind`,#nr=`@constrnr`, #args = $argtypes, #vis=`Visible/Int`,
       #fnr=`@formatnr`, #loci=$loci); 
  } 
  pkeyword(#str=" for "); 

  pp(#k=`@constrkind`,#nr=`@constrnr`, #args = $argtypes,
  #pid=`@redefnr`, #loci=$loci); ";"; <br;

}

// ignore forgetful functors - unhandled yet
tpl [Notations/Pattern] {
// pp1(#k=`@constrkind`,#nr=`@constrnr`,#vis=`Visible/Int`,
// #fnr=`@formatnr`, #loci="1"); <br;
   if [not(@kind = "J")]
   {
      apply[ArgTypes];

      if[Expansion]
      {

//	     $alc = lc(#s=`@aid`);
	     $sym = abs1(#k = "M", #fnr = `@formatnr`);
	     pkeyword(#str="mode ");  

	     absref(#elems = `.`, #c = "0", #sym = $sym, #pid = `@relnr`);

// 	     <a 
// 	     { 
// 	        @href=`concat($alc, ".", $ext, "#","NM",@nr)`; 
// 		if [$titles="1"] { @title=`concat(@aid,":","NM",".",@nr)`; }
// 		abs1(#k = "M", #fnr = `@formatnr`);
// 	     }

	     if [Visible/Int] 
	     { 
	        " of "; 
		for-each [Visible/Int] 
		{ 
		   ploci(#nr=`@x`); 
		   if [not(position()=last())] { ","; } 
                }
             }

	     pkeyword(#str=" is "); 
          
 
	  apply[Expansion/Typ]; ";"; 
	  <br; 
      }
      else 
      {
         $loci = { if [$mml="1"] { "1"; } else { "2"; }}
	 $mk = { mkind(#kind=`@kind`); }

	 pkeyword(#str=$mk); " ";
	 pp1(#k=`@constrkind`,#nr=`@constrnr`,#vis=`Visible/Int`,
	     #fnr=`@formatnr`, #loci="1"); 

	 <br;

      }

      <br;
}
}

// ignore normal Patterns now
tpl [Pattern] {}

// Default
tpl [/] { if [$generate_items = "1"] { 
    apply[/*/JustifiedTheorem|/*/DefTheorem|/*/SchemeBlock];
    apply[//RCluster|//CCluster|//FCluster|//Definition|//IdentifyWithExp];
// top-level lemmas
   for-each [/*/Proposition] 
   {
// <xsl:document href="proofhtml/lemma/{$anamelc}.{@propnr}" format="html">
      apply[`.`];
// </xsl:document>
   $bogus=`1`;
   } 
}

else { 
  if [$body_only = "0"] { 
    <html { @prefix="oo: http://omdoc.org/ontology# owl: http://www.w3.org/2002/07/owl#";

// output the css defaults for div and p (for indenting)
        <style { @type="text/css";  "
div { padding: 0 0 0 0; margin: 0 0 0 0; } 
div.add { padding-left: 3mm; padding-bottom: 0mm;  margin: 0 0 0 0; } 
div.box { border-width:thin; border-color:blue; border-style:solid; }
p { margin: 0 0 0 0; } 
body {font-family: monospace; margin: 0px;}
a {text-decoration:none} a:hover { color: red; } 
a.ref { font-size:x-small; }
a.ref:link { color:green; } 
a.ref:hover { color: red; } 
a.txt:link { color:black; } 
a.txt:hover { color: red; } 
.wikiactions ul { background-color: DarkSeaGreen ; color:blue; margin: 0; padding: 6px; list-style-type: none; border-bottom: 1px solid #000; }
.wikiactions li { display: inline; padding: .2em .4em; }
.wikiactions a {text-decoration:underline;} 
span.kw {font-weight: bold; }
span.lab {font-style: italic; }
span.comment {font-style: italic; }
span.hide { display: none; }
span.p1:hover { color : inherit; background-color : #BAFFFF; } 
span.p2:hover { color : inherit; background-color : #FFCACA; }
span.p3:hover { color : inherit; background-color : #FFFFBA; }
span.p4:hover { color : inherit; background-color : #CACAFF; }
span.p5:hover { color : inherit; background-color : #CAFFCA; }
span.p0:hover { color : inherit; background-color : #FFBAFF; }
.default { background-color: white; color: black; } 
.default:hover { background-color: white; color: black; }
#tt { position:absolute; display:block; font-size: small; background: LightYellow; padding:2px 12px 3px 7px; margin-left:5px;}
:target { background: #5D9BF7; border: solid 1px #aaa;}
";
	                } 
        <head {  
<title { 
  if [$mk_header > 0]
  {
     $aname; ": "; for-each [document($hdr,/)/Header/dc:title] { `text()`; }
  }
  else { $aname; }}
<script { @type="text/javascript";

"
<!-- 

// for saving in rs
var mizhtm='"; $mizhtml; "';"; 
$mizjs1;
  }

<script { @type="text/x-mathjax-config";
"
  MathJax.Hub.Config({                                                                                                                            
    extensions: ['tex2jax.js'],                                                                                                                   
    jax: ['input/TeX', 'output/HTML-CSS'],                                                                                                        
    tex2jax: {                                                                                                                                    
      inlineMath: [ ['$','$'], ['\\(','\\)'] ],                                                                                                   
      displayMath: [ ['$$','$$'], ['\\[','\\]'] ],                                                                                                
  processClass: 'mathjax',                                                                                                                        
  ignoreClass: 'no-mathjax',                                                                                                                      
      processEscapes: true,                                                                                                                       
    },                                                                                                                                            
    'HTML-CSS': {   scale: 80, availableFonts: ['TeX'] }                                                                                          
  });
";
}
<script { @type="text/javascript";
   @src="https://cdn.mathjax.org/mathjax/latest/MathJax.js";
}
  
}
        <body {  @class="no-mathjax";

	if[$wiki_links=1]
	{
	   <div 
	   {  
	      @class="wikiactions";
	      <ul
	      {
	        <li {  <a { @href=`concat($lmwikicgi,"?p=",$lgitproject,";a=edit;f=mml/",$anamelc,".miz")`; @rel="nofollow"; "Edit"; } }
	        <li {  <a { @href=`concat($lmwikicgi,"?p=",$lgitproject,";a=history;f=mml/",$anamelc,".miz")`; "History"; } }
		<li {  <a { @href=`concat($lmwikicgi,"?p=",$lgitproject,";a=blob_plain;f=mml/",$anamelc,".miz")`; @rel="nofollow"; "Raw"; } }
//		<li {  <a { @href=`concat("../discussion/",$anamelc, ".html")`; "Discussion"; } }
		<li {  <a { @href=$lmwikiindex; "Index"; } }
		<li {  <a { @href=`concat($lmwikicgi,"?p=",$lgitproject,";a=gitweb")`; "Gitweb"; } }
//		<li {  "Clone:"; $lgitclone; <br; }
               }
            }
        }

	if[$mk_header > 0] { apply[document($hdr,/)/Header/*]; <br; }
	if[$mk_environ > 0] { pkeyword(#str="environ "); <br;  <br; apply[document($evl,/)/Environ/*]; <br; }

// first read the keys for imported stuff
//          apply[document($constrs,/)/Constructors/Constructor]; 
//          apply[document($thms,/)/Theorems/Theorem]; 
//          apply[document($schms,/)/Schemes/Scheme];
 
// then process the whole document
          apply; }}}
  
     // $body_only > 0
     else 
     {
       if[$mk_header > 0] { apply[document($hdr,/)/Header/*]; <br; }
       	if[$mk_environ > 0] { pkeyword(#str="environ "); <br; <br;  apply[document($evl,/)/Environ/*]; <br; }
       apply;
     }
  }
}
  
// tpl [*] { copy { apply [@*]; apply; } }
// tpl [@*] { copy-of `.`; }

// Header rules
tpl [dc:title] { pcomment(#str=`text()`); }
tpl [dc:creator] { pcomment(#str=`concat("by ", text())`); pcomment(#str=""); }
tpl [dc:date] { pcomment(#str=`concat("Received ", text())`); }
tpl [dc:rights] { pcomment(#str=`concat("Copyright ", text())`); }

tpl [Directive] { pkeyword(#str=`@name`); " "; list(#separ=", ", #elems=`Ident`); ";"; <br; }
tpl [Ident] { aidref(#aid=`@name`);}
    
// comment rules

tpl [Comment] 
{ 
   <div { @class="comment mathjax";
   	if [$colored="1"] {
          <font {@color=$commentcolor; apply; }
     	}
     	else {  apply; }
   }
}
tpl [CmtLine]  { `text()`; <br; }
tpl [CmtLink]  { ":: "; add_wp_icon(); " "; for-each [*] { copy { copy-of `@*`; copy-of `text()`;}} <br; }

tpl add_wp_icon
{
     <img
     {
       	       @src= `concat($ltptproot,"WP.ico")`;
       	       @alt= "WP: ";
     }
}