☰

newLISP Documentation Search

Provide keyword search interface in newLISP documentation

目前為 2014-10-01 提交的版本，檢視 最新版本。

  1. // ==UserScript==
  2. // @name      newLISP Documentation Search
  3. // @namespace http://lambda.que.jp/
  4. // @version   20141001
  5. // @description  Provide keyword search interface in newLISP documentation
  6. // @grant   GM_addStyle
  7. // @grant   GM_getResourceText
  8. // @match   http://www.newlisp.org/*/newlisp_manual.html
  9. // @require http://code.jquery.com/jquery-2.1.1.js
  10. // @require http://code.jquery.com/ui/1.11.1/jquery-ui.js
  11. // @resource jquery-ui.css http://code.jquery.com/ui/1.11.1/themes/smoothness/jquery-ui.css
  12. // @author  KOBAYASHI Shigeru (kosh)
  13. // @license Public Domain
  14. // ==/UserScript==
  15.  
  16. GM_addStyle([
  17.     GM_getResourceText("jquery-ui.css"),
  18.     ".search-control {",
  19.     "  position: fixed;",
  20.     "  top: 10px;",
  21.     "  right: 20px;",
  22.     "}",
  23.     ".ui-autocomplete {",
  24.     "  max-height: 100px;",
  25.     "  overflow-x: hidden;",
  26.     "  overflow-y: auto;",
  27.     "}",
  28. ].join("\n"));
  29.  
  30. $("body").prepend([
  31.     "<div class='search-control ui-widget' role='search'>",
  32.     " <label for='keyword' style='display:none;'>Search:</label>",
  33.     " <input id='keyword' type='search' placeholder='Search keyword' autofocus>",
  34.     "</div>",
  35. ].join("\n"));
  36.  
  37. function create_keywords() {
  38.     var keywords = [],
  39.         grep = function(obj, key, value) {
  40.         return $.grep(obj, function(e) { return e[key] === value; });
  41.     };
  42.  
  43.     $("a[href]").each(function(i, a) {
  44.         var hash = a.hash.slice(1), // #hash -> hash
  45.             href = a.href;
  46.         if (hash.length == 0 || grep(keywords, "href", href).length > 0) {
  47.             return;
  48.         }
  49.         keywords.push({ "label": hash, "href":  href });
  50.     });
  51.  
  52.     return keywords;
  53. }
  54.  
  55. $("#keyword").autocomplete({
  56.     source: create_keywords(),
  57.     select: function(event, ui) {
  58.         window.location.replace(ui.item.href);
  59.     }
  60. });