Docs: Add AJAX search field to the docs

Docs: Add AJAX search field to the docs

-) Add a search field to the toc pane in our docs. If the user types three
   letters or more, an AJAX request is sent to the server to perform a
   search. The AJAX part is implemented in JS, the search part itself is
   implemented in PHP on the server side, which wades through a pre-generated
   index file (pure text).
-) The texi2html init file now has the ability to create our own search
   index file, currently in pure text (the search script will go through it
   line for line.
-) The search box is shown via JavaScript only if the files are viewed over
   http. If the user has JavaScript disabled or if the files are viewed as
   static pages (and not over http), then no search box appears, since it
   would not work anyway.
-) Also, don't show search box when AJAX initialization failed.
-) Print nice message if search index can't be opened, don't fail with error
-) Install and use language-dependent index files for all known languages
-) If we don't have a texinfo index, don't load the JS and don't print
   out the search box. (Workaround: css_lines is called before
   init_out, so we need to do the check already in css_lines!)
   If the index would be empty, don't create an empty .idx file

-) If AJAX works and a user presses enter, the same AJAX query is triggered
   as when entering some letters, and the results appear on the same page.
   However, if for some reason AJAX does not work (in particular, if the
   onSubmit action handler isn't called), then a search page is loaded
   with the same results as the AJAX query...