1901 </xsl:text>

  1901 </xsl:text>

  1902     <xsl:text>

  1902     <xsl:text>

  1903 </xsl:text>

  1903 </xsl:text>

  1904     <xsl:text>    jump_history.push([page_name, page_index]);

  1904     <xsl:text>    jump_history.push([page_name, page_index]);

  1905 </xsl:text>

  1905 </xsl:text>

  1906     <xsl:text>

  1910     <xsl:text>

  1907 </xsl:text>

  1911 </xsl:text>

  1908     <xsl:text>    return true;

  1912     <xsl:text>    return true;

  1909 </xsl:text>

  1913 </xsl:text>

  1910     <xsl:text>};

  1914     <xsl:text>};