diff options
author | Gilles Dubochet <gilles.dubochet@epfl.ch> | 2010-06-18 15:34:35 +0000 |
---|---|---|
committer | Gilles Dubochet <gilles.dubochet@epfl.ch> | 2010-06-18 15:34:35 +0000 |
commit | cb367e28eed815419d29fb73acb2d66c7d3ecb3f (patch) | |
tree | bdd823ad2269749cd59d3fb0ae91a1f2cd118c7c /src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css | |
parent | 9923b97157725ae1f7853a4834ef5e31283a1b98 (diff) | |
download | scala-cb367e28eed815419d29fb73acb2d66c7d3ecb3f.tar.gz scala-cb367e28eed815419d29fb73acb2d66c7d3ecb3f.tar.bz2 scala-cb367e28eed815419d29fb73acb2d66c7d3ecb3f.zip |
[scaladoc] There is a text filter tool for memb...
[scaladoc] There is a text filter tool for members (searching on member
name and comment body). Adds button to reset text filter tool. No
review.
Known limitation: filtering of members is blocking on keystroke leading
to sluggish performance on large classes. Scheduler from index needs to
be used for member filtering.
Diffstat (limited to 'src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css')
-rw-r--r-- | src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css | 37 |
1 files changed, 23 insertions, 14 deletions
diff --git a/src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css b/src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css index fc3f6d4c29..0d30662da6 100644 --- a/src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css +++ b/src/compiler/scala/tools/nsc/doc/html/resource/lib/index.css @@ -47,30 +47,39 @@ h1 { #textfilter { position: relative; display: block; + height: 20px; + margin-bottom: 5px; } -#textfilter:before { +#textfilter > .pre { display: block; - content: url("filter_box_left.png"); + position: absolute; + top: 0; + left: 0; + height: 20px; + width: 20px; + background: url("filter_box_left.png"); } -#textfilter:after { +#textfilter > .post { display: block; - position: absolute; - top: 0; - right: 0; - content: url("filter_box_right.png"); + position: absolute; + top: 0; + right: 0; + height: 20px; + width: 20px; + background: url("filter_box_right.png"); } #textfilter input { display: block; - position: absolute; - top: 0; - left: 32px; - right: 16px; - height: 22px; - width: 232px; - padding: 5px; + position: absolute; + top: 0; + right: 20px; + left: 20px; + height: 16px; + width: 246px; + padding: 2px; font-weight: bold; color: #993300; background-color: white; |