Re: CSS enhancements

[Shigio YAMAGUCHI]

Hello,

2013/10/22 Mooffie <address@hidden>

(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 }

Good idea. I will take this solution.

Thank you for the useful advice, 

(2) The second problem is when we browse many files. The titles in the
...
The solution is simple: make the filename clearly shown in the page
itself. Currently, the <h2> header (which contains the filename)

Now, is it useless?

htags --fixed-guide

The --fixed-guide put a fixed guide at the bottom of the screen

of the browser. It includes the path name of the source file.

Shigio
-- 

Shigio YAMAGUCHI <address@hidden>

PGP fingerprint: D1CB 0B89 B346 4AB6 5663  C4B6 3CA5 BBB3 57BE DDA3