<div dir="ltr">What about the patch in attachment?</div><div class="gmail_extra"><br><div class="gmail_quote">2015-10-08 1:54 GMT+03:00 Barry Smith <span dir="ltr"><<a href="mailto:bsmith@mcs.anl.gov" target="_blank">bsmith@mcs.anl.gov</a>></span>:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class=""><br>
> On Sep 30, 2015, at 7:46 AM, Stefano Zampini <<a href="mailto:stefano.zampini@gmail.com">stefano.zampini@gmail.com</a>> wrote:<br>
><br>
> I just noticed that Figures 19 and 20 in the manual (current release and master) are messed up. The htmlmap process seems not to work properly.<br>
<br>
</span>The tool /bin/maint/mapnameslatex.py is what looks through the tokens in the .tex files and replaces PETSc functions etc with an href. Unfortunately it is simple minded. It should turn off replacement when it detects a \begin{verbatim} and turn it back on when it hits the \end{verbatim} here is the entire engine<br>
<br>
    while 1:<br>
        token = lex.token()       # Get a token<br>
        if not token: break        # No more tokens<br>
        if token.type == 'NEWLINE':<br>
            print text<br>
            text = ''<br>
        else:<br>
            # \href cannot be used in many places in Latex<br>
            if token.value in ['\\href{','\\findex{','\\sindex{','\\subsection{','\\chapter{','\\section{','\\caption{','\\trl{']:<br>
                bracket = bracket + 1;<br>
            if bracket == 0:<br>
                value = token.value<br>
                if mappedstring.has_key(value):<br>
                    mvalue = mappedstring[value].replace('_','\\_')<br>
                    value = '\\href{'+'<a href="http://www.mcs.anl.gov/petsc/petsc-'+version+'/docs/'+mappedlink[value]+'}{'+mvalue+'" rel="noreferrer" target="_blank">http://www.mcs.anl.gov/petsc/petsc-'+version+'/docs/'+mappedlink[value]+'}{'+mvalue+'</a>}\\findex{'+value+'}'<br>
            else:<br>
                value = token.value<br>
            if token.value[0] == '}' and bracket:<br>
                bracket = bracket - 1;<br>
            text = text+value<br>
<br>
You want to take a crack at fixing it? Because I don't really feel like it :-(<br>
<span class="HOEnZb"><font color="#888888"><br>
  Barry<br>
<br>
<br>
<br>
><br>
> --<br>
> Stefano<br>
<br>
</font></span></blockquote></div><br><br clear="all"><div><br></div>-- <br><div class="gmail_signature">Stefano</div>
</div>