diff options
Diffstat (limited to 'html')
| -rw-r--r-- | html/frames.html | 27 | ||||
| -rw-r--r-- | html/haddock-util.js | 6 | ||||
| -rw-r--r-- | html/haddock.css | 30 | 
3 files changed, 63 insertions, 0 deletions
| diff --git a/html/frames.html b/html/frames.html new file mode 100644 index 00000000..9e904fc1 --- /dev/null +++ b/html/frames.html @@ -0,0 +1,27 @@ +<html>
 +<head>
 +<script type="text/javascript"><!--
 +/*
 +
 +  The synopsis frame needs to be updated using javascript, so we hide
 +  it by default and only show it if javascript is enabled.
 +
 +  TODO: provide some means to disable it.
 +*/
 +function load() {
 +  var d = document.getElementById("inner-fs");
 +  d.rows = "50%,50%";
 +}
 +--></script>
 +<frameset id="outer-fs" cols="25%,75%" onload="load()">
 +  <frameset id="inner-fs" rows="100%,0%">
 +
 +    <frame src="index-frames.html" name="modules">
 +    <frame src="" name="synopsis">
 +
 +  </frameset>
 +  <frame src="index.html" name="main">
 +
 +</frameset>
 +
 +</html>
 diff --git a/html/haddock-util.js b/html/haddock-util.js index e5d6977e..364081f0 100644 --- a/html/haddock-util.js +++ b/html/haddock-util.js @@ -131,3 +131,9 @@ function perform_search(full)          return ""; // should never be reached      }  } + +function setSynopsis(filename) { +    if (parent.window.synopsis) { +      parent.window.synopsis.location = filename; +    } +} diff --git a/html/haddock.css b/html/haddock.css index 26695270..35a078d1 100644 --- a/html/haddock.css +++ b/html/haddock.css @@ -4,6 +4,7 @@ BODY {    background-color: #ffffff;    color: #000000;    font-family: sans-serif; +  padding: 0 0;    }   A:link    { color: #0000e0; text-decoration: none } @@ -265,3 +266,32 @@ TD.botbar A:hover {    background-color: #6060ff    } +/* --------- Mini Synopsis for Frame View --------- */ + +.outer { +  margin: 0 0; +  padding: 0 0; +} + +.mini-synopsis { +  padding: 0.25em 0.25em; +} + +.mini-synopsis H1 { font-size: 130%; } +.mini-synopsis H2 { font-size: 110%; } +.mini-synopsis H3 { font-size: 100%; } +.mini-synopsis H1, .mini-synopsis H2, .mini-synopsis H3 { +  margin-top: 0.5em; +  margin-bottom: 0.25em; +  padding: 0 0; +} + +.mini-synopsis H1 { border-bottom: 1px solid #ccc; } + +.mini-topbar { +  font-size: 130%; +  background: #0077dd; +  padding: 0.25em; +} + + | 
