CSS enhancements

[Mooffie]

The are two usability problems in the HTML that can be easily solved with CSS:

See the screenshot:

http://oi42.tinypic.com/11lpmv7.jpg
(It the link doesn't work, try http://tinypic.com/view.php?pic=11lpmv7&s=5 )

(1) The first problem is when we jump to a specific line in a file
(using anchor). The browser adjusts the view so that the line is at
the top, but if the line is close to the end of the file, this doesn't
quite work. It's a known problem. The solution is to highlight the
line number, e.g. by doing:

  a:target { background: yellow }

The pink arrow (numbered "1") shows the result.

This has many advantages: we can browse the file and not "forget" why
we're there.

(2) The second problem is when we browse many files. The titles in the
browser's tabs become so short we don't see the file names (see the
screenshot: the tabs say "lib/widg..." and we can't see the actual
file names). So since we don't know what files are open, instead of
switching to their existing tabs we open new files. So we have even
more tabs. It's a cycle: We open more and more files, which is a
reason for more and more tabs, which is the reason for opening yet
more files, which gives us more tabs. A lot of mess.

The solution is simple: make the filename clearly shown in the page
itself. Currently, the <h2> header (which contains the filename)
appears at the top of the page so we usually *don't* see it. The
solution is to "fix" it so it's always visible:

  .header:nth-child(2) { position: fixed; right: 1em; top: 2em; }

(BTW, the HTML should better output some distinctive CSS class for
this element so that we shouldn't need to use the "nth-child(2)"
hack.)

(We can also fix it to the lower right corner instead of the top right.)

On my system (see pink arrow "2") I used a more daring CSS:

  .header:nth-child(2) { position: fixed; background: white; padding:
0.6em; border: 1px solid black; right: 6em; top: 4.5em; }

(This makes it closer to the center of the page so I don't need to
move my head to read the file name. This is *very* convenient. But
this variation is perhaps too daring for a default setup.)

Bye.