docs search function: give a boost to built-in types and functions

Author: adqm

Doc/conf.py

@@ -575,3 +575,8 @@
         '<meta property="og:image:width" content="200">',
         '<meta property="og:image:height" content="200">',
     )
+
+# Options to adjust search results sorting
+# ----------------------------------------
+
+html_search_scorer = "search_scorer.js"

Doc/search_scorer.js

@@ -0,0 +1,24 @@
+var Scorer = {
+  score: function (result) {
+    let [docname, title, anchor, descr, score, filename] = result;
+    if (docname == "library/stdtypes" || docname == "library/functions") {
+      score += 10;
+    }
+    return score;
+  },
+
+  objPrio: {
+    0: 15,
+    1: 5,
+    2: -5,
+  },
+  objPrioDefault: 0,
+
+  objNameMatch: 20,
+  objPartialMatch: 6,
+
+  title: 15,
+  partialTitle: 7,
+  term: 5,
+  partialTerm: 2,
+};