<script src="//ajax.googleapis.com/ajax/libs/jquery/1.9.1/jquery.min.js"></script>
<script type="text/javascript" src="script.js"></script>
</head>
-<body>\n"""
+<body>
+<div id="header">
+ <div id="requesters-filter">Filter by requesters:<br></div>
+</div>
+<div id="content">
+"""
)
self.requests.reverse()
for r in self.requests:
r.dump_html(f)
self.requests.reverse()
- f.write("</body></html>\n")
+ f.write("</div></body></html>\n")
f.flush()
os.fsync(f.fileno())
f.close()
}
});
- var $filter = $('<div id=requesters-filter>Filter by requesters:<br></div>');
- $('body').prepend($filter);
+ var $filter = $('#requesters-filter');
+ if ($filter.length == 0) {
+ $filter = $('<div id=requesters-filter>Filter by requesters:<br></div>');
+ $('body').prepend($filter);
+ }
requesters.forEach(function(r) {
var $button = $('<button class=request-filter>'+ r + '</button>');
$button.on('click', function() {
position: relative;
}
- div {
+ div.request {
background-color: white;
margin: 10px 0px;
padding: 2px;
background-color: #ffffcc;
color: black;
}
+
+ #header {
+ background-color: white;
+ border: 1px solid black;
+ padding: 0.5em;
+ position: fixed;
+ z-index: 100;
+ }
+
+ #content {
+ clear: both;
+ margin-top: 5em;
+ overflow: auto;
+ position: absolute;
+ width: 100%;
+ }
}
@media print {
a {
background-color: inherit;
color: inherit;
}
+ #header {
+ display: none;
+ }
}
@media projection {