1235 </xsl:text>

  1235 </xsl:text>

  1236     <xsl:text>

  1236     <xsl:text>

  1237 </xsl:text>

  1237 </xsl:text>

  1238     <xsl:text>    svg_root.setAttribute('viewBox',new_desc.bbox.join(" "));

  1238     <xsl:text>    svg_root.setAttribute('viewBox',new_desc.bbox.join(" "));

  1239 </xsl:text>

  1239 </xsl:text>

  1242     <xsl:text>    current_page = page_name;

  1240     <xsl:text>    current_page = page_name;

  1243 </xsl:text>

  1241 </xsl:text>

  1244     <xsl:text>

  1242     <xsl:text>

  1245 </xsl:text>

  1243 </xsl:text>

  1246     <xsl:text>    window.setTimeout(update_subscriptions,0);

  1244     <xsl:text>    window.setTimeout(update_subscriptions,0);