diff options
| -rw-r--r-- | html/Ocean.std-theme/ocean.css | 5 | ||||
| -rw-r--r-- | html/haddock-util.js | 8 | 
2 files changed, 10 insertions, 3 deletions
| diff --git a/html/Ocean.std-theme/ocean.css b/html/Ocean.std-theme/ocean.css index 205b8e6e..e683efcc 100644 --- a/html/Ocean.std-theme/ocean.css +++ b/html/Ocean.std-theme/ocean.css @@ -296,6 +296,11 @@ div#style-menu-holder {  }  #synopsis { +  display: none; +} + +.no-frame #synopsis { +  display: block;    position: fixed;    right: 0;    height: 80%; diff --git a/html/haddock-util.js b/html/haddock-util.js index cd18aa81..8d43b996 100644 --- a/html/haddock-util.js +++ b/html/haddock-util.js @@ -212,15 +212,17 @@ function addMenuItem(html) {  }  function adjustForFrames() { +  var bodyCls; +      if (parent.location.href == window.location.href) {      // not in frames, so add Frames button      addMenuItem("<a href='#' onclick='reframe();return true;'>Frames</a>"); +    bodyCls = "no-frame";    }    else { -    // in frames, remove synopsis -    var syn = document.getElementById("synopsis"); -    if (syn) { syn.parentNode.removeChild(syn); } +    bodyCls = "in-frame";    } +  addClass(document.body, bodyCls);  }  function reframe() { | 
