411 document.getElementsByTagName('head')[0].appendChild(css); |
411 document.getElementsByTagName('head')[0].appendChild(css); |
412 }})()""" |
412 }})()""" |
413 style = css.replace("'", "\\'").replace("\n", "\\n") |
413 style = css.replace("'", "\\'").replace("\n", "\\n") |
414 return source.format(style) |
414 return source.format(style) |
415 |
415 |
|
416 |
|
417 def scrollToAnchor(anchor): |
|
418 """ |
|
419 Function generating script to scroll to a given anchor. |
|
420 |
|
421 @param anchor name of the anchor to scroll to |
|
422 @type str |
|
423 @return script to set the style sheet |
|
424 @rtype str |
|
425 """ |
|
426 source = """ |
|
427 (function() {{ |
|
428 var e = document.getElementById("{0}") |
|
429 if (!e) {{ |
|
430 var els = document.querySelectorAll("[name='{0}']"); |
|
431 if (els.length) |
|
432 e = els[0] |
|
433 }} |
|
434 if (e) |
|
435 e.scrollIntoView() |
|
436 }})()""" |
|
437 return source.format(anchor) |
|
438 |
416 ########################################################################### |
439 ########################################################################### |
417 ## scripts below are specific for eric |
440 ## scripts below are specific for eric |
418 ########################################################################### |
441 ########################################################################### |
419 |
442 |
420 |
443 |