Contact
CoCalc Logo Icon
StoreFeaturesDocsShareSupport News AboutSign UpSign In
| Download

Reference manual of the SageMath package kerrgeodesic_gw

Project: Sagittarius
Views: 7653
License: GPL3
Image: ubuntu2004
1
/*
2
* searchtools.js
3
* ~~~~~~~~~~~~~~~~
4
*
5
* Sphinx JavaScript utilities for the full-text search.
6
*
7
* :copyright: Copyright 2007-2021 by the Sphinx team, see AUTHORS.
8
* :license: BSD, see LICENSE for details.
9
*
10
*/
11
12
if (!Scorer) {
13
/**
14
* Simple result scoring code.
15
*/
16
var Scorer = {
17
// Implement the following function to further tweak the score for each result
18
// The function takes a result array [filename, title, anchor, descr, score]
19
// and returns the new score.
20
/*
21
score: function(result) {
22
return result[4];
23
},
24
*/
25
26
// query matches the full name of an object
27
objNameMatch: 11,
28
// or matches in the last dotted part of the object name
29
objPartialMatch: 6,
30
// Additive scores depending on the priority of the object
31
objPrio: {0: 15, // used to be importantResults
32
1: 5, // used to be objectResults
33
2: -5}, // used to be unimportantResults
34
// Used when the priority is not in the mapping.
35
objPrioDefault: 0,
36
37
// query found in title
38
title: 15,
39
partialTitle: 7,
40
// query found in terms
41
term: 5,
42
partialTerm: 2
43
};
44
}
45
46
if (!splitQuery) {
47
function splitQuery(query) {
48
return query.split(/\s+/);
49
}
50
}
51
52
/**
53
* Search Module
54
*/
55
var Search = {
56
57
_index : null,
58
_queued_query : null,
59
_pulse_status : -1,
60
61
htmlToText : function(htmlString) {
62
var virtualDocument = document.implementation.createHTMLDocument('virtual');
63
var htmlElement = $(htmlString, virtualDocument);
64
htmlElement.find('.headerlink').remove();
65
docContent = htmlElement.find('[role=main]')[0];
66
if(docContent === undefined) {
67
console.warn("Content block not found. Sphinx search tries to obtain it " +
68
"via '[role=main]'. Could you check your theme or template.");
69
return "";
70
}
71
return docContent.textContent || docContent.innerText;
72
},
73
74
init : function() {
75
var params = $.getQueryParameters();
76
if (params.q) {
77
var query = params.q[0];
78
$('input[name="q"]')[0].value = query;
79
this.performSearch(query);
80
}
81
},
82
83
loadIndex : function(url) {
84
$.ajax({type: "GET", url: url, data: null,
85
dataType: "script", cache: true,
86
complete: function(jqxhr, textstatus) {
87
if (textstatus != "success") {
88
document.getElementById("searchindexloader").src = url;
89
}
90
}});
91
},
92
93
setIndex : function(index) {
94
var q;
95
this._index = index;
96
if ((q = this._queued_query) !== null) {
97
this._queued_query = null;
98
Search.query(q);
99
}
100
},
101
102
hasIndex : function() {
103
return this._index !== null;
104
},
105
106
deferQuery : function(query) {
107
this._queued_query = query;
108
},
109
110
stopPulse : function() {
111
this._pulse_status = 0;
112
},
113
114
startPulse : function() {
115
if (this._pulse_status >= 0)
116
return;
117
function pulse() {
118
var i;
119
Search._pulse_status = (Search._pulse_status + 1) % 4;
120
var dotString = '';
121
for (i = 0; i < Search._pulse_status; i++)
122
dotString += '.';
123
Search.dots.text(dotString);
124
if (Search._pulse_status > -1)
125
window.setTimeout(pulse, 500);
126
}
127
pulse();
128
},
129
130
/**
131
* perform a search for something (or wait until index is loaded)
132
*/
133
performSearch : function(query) {
134
// create the required interface elements
135
this.out = $('#search-results');
136
this.title = $('<h2>' + _('Searching') + '</h2>').appendTo(this.out);
137
this.dots = $('<span></span>').appendTo(this.title);
138
this.status = $('<p class="search-summary">&nbsp;</p>').appendTo(this.out);
139
this.output = $('<ul class="search"/>').appendTo(this.out);
140
141
$('#search-progress').text(_('Preparing search...'));
142
this.startPulse();
143
144
// index already loaded, the browser was quick!
145
if (this.hasIndex())
146
this.query(query);
147
else
148
this.deferQuery(query);
149
},
150
151
/**
152
* execute search (requires search index to be loaded)
153
*/
154
query : function(query) {
155
var i;
156
157
// stem the searchterms and add them to the correct list
158
var stemmer = new Stemmer();
159
var searchterms = [];
160
var excluded = [];
161
var hlterms = [];
162
var tmp = splitQuery(query);
163
var objectterms = [];
164
for (i = 0; i < tmp.length; i++) {
165
if (tmp[i] !== "") {
166
objectterms.push(tmp[i].toLowerCase());
167
}
168
169
if ($u.indexOf(stopwords, tmp[i].toLowerCase()) != -1 || tmp[i] === "") {
170
// skip this "word"
171
continue;
172
}
173
// stem the word
174
var word = stemmer.stemWord(tmp[i].toLowerCase());
175
// prevent stemmer from cutting word smaller than two chars
176
if(word.length < 3 && tmp[i].length >= 3) {
177
word = tmp[i];
178
}
179
var toAppend;
180
// select the correct list
181
if (word[0] == '-') {
182
toAppend = excluded;
183
word = word.substr(1);
184
}
185
else {
186
toAppend = searchterms;
187
hlterms.push(tmp[i].toLowerCase());
188
}
189
// only add if not already in the list
190
if (!$u.contains(toAppend, word))
191
toAppend.push(word);
192
}
193
var highlightstring = '?highlight=' + $.urlencode(hlterms.join(" "));
194
195
// console.debug('SEARCH: searching for:');
196
// console.info('required: ', searchterms);
197
// console.info('excluded: ', excluded);
198
199
// prepare search
200
var terms = this._index.terms;
201
var titleterms = this._index.titleterms;
202
203
// array of [filename, title, anchor, descr, score]
204
var results = [];
205
$('#search-progress').empty();
206
207
// lookup as object
208
for (i = 0; i < objectterms.length; i++) {
209
var others = [].concat(objectterms.slice(0, i),
210
objectterms.slice(i+1, objectterms.length));
211
results = results.concat(this.performObjectSearch(objectterms[i], others));
212
}
213
214
// lookup as search terms in fulltext
215
results = results.concat(this.performTermsSearch(searchterms, excluded, terms, titleterms));
216
217
// let the scorer override scores with a custom scoring function
218
if (Scorer.score) {
219
for (i = 0; i < results.length; i++)
220
results[i][4] = Scorer.score(results[i]);
221
}
222
223
// now sort the results by score (in opposite order of appearance, since the
224
// display function below uses pop() to retrieve items) and then
225
// alphabetically
226
results.sort(function(a, b) {
227
var left = a[4];
228
var right = b[4];
229
if (left > right) {
230
return 1;
231
} else if (left < right) {
232
return -1;
233
} else {
234
// same score: sort alphabetically
235
left = a[1].toLowerCase();
236
right = b[1].toLowerCase();
237
return (left > right) ? -1 : ((left < right) ? 1 : 0);
238
}
239
});
240
241
// for debugging
242
//Search.lastresults = results.slice(); // a copy
243
//console.info('search results:', Search.lastresults);
244
245
// print the results
246
var resultCount = results.length;
247
function displayNextItem() {
248
// results left, load the summary and display it
249
if (results.length) {
250
var item = results.pop();
251
var listItem = $('<li></li>');
252
var requestUrl = "";
253
var linkUrl = "";
254
if (DOCUMENTATION_OPTIONS.BUILDER === 'dirhtml') {
255
// dirhtml builder
256
var dirname = item[0] + '/';
257
if (dirname.match(/\/index\/$/)) {
258
dirname = dirname.substring(0, dirname.length-6);
259
} else if (dirname == 'index/') {
260
dirname = '';
261
}
262
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + dirname;
263
linkUrl = requestUrl;
264
265
} else {
266
// normal html builders
267
requestUrl = DOCUMENTATION_OPTIONS.URL_ROOT + item[0] + DOCUMENTATION_OPTIONS.FILE_SUFFIX;
268
linkUrl = item[0] + DOCUMENTATION_OPTIONS.LINK_SUFFIX;
269
}
270
listItem.append($('<a/>').attr('href',
271
linkUrl +
272
highlightstring + item[2]).html(item[1]));
273
if (item[3]) {
274
listItem.append($('<span> (' + item[3] + ')</span>'));
275
Search.output.append(listItem);
276
setTimeout(function() {
277
displayNextItem();
278
}, 5);
279
} else if (DOCUMENTATION_OPTIONS.HAS_SOURCE) {
280
$.ajax({url: requestUrl,
281
dataType: "text",
282
complete: function(jqxhr, textstatus) {
283
var data = jqxhr.responseText;
284
if (data !== '' && data !== undefined) {
285
listItem.append(Search.makeSearchSummary(data, searchterms, hlterms));
286
}
287
Search.output.append(listItem);
288
setTimeout(function() {
289
displayNextItem();
290
}, 5);
291
}});
292
} else {
293
// no source available, just display title
294
Search.output.append(listItem);
295
setTimeout(function() {
296
displayNextItem();
297
}, 5);
298
}
299
}
300
// search finished, update title and status message
301
else {
302
Search.stopPulse();
303
Search.title.text(_('Search Results'));
304
if (!resultCount)
305
Search.status.text(_('Your search did not match any documents. Please make sure that all words are spelled correctly and that you\'ve selected enough categories.'));
306
else
307
Search.status.text(_('Search finished, found %s page(s) matching the search query.').replace('%s', resultCount));
308
Search.status.fadeIn(500);
309
}
310
}
311
displayNextItem();
312
},
313
314
/**
315
* search for object names
316
*/
317
performObjectSearch : function(object, otherterms) {
318
var filenames = this._index.filenames;
319
var docnames = this._index.docnames;
320
var objects = this._index.objects;
321
var objnames = this._index.objnames;
322
var titles = this._index.titles;
323
324
var i;
325
var results = [];
326
327
for (var prefix in objects) {
328
for (var name in objects[prefix]) {
329
var fullname = (prefix ? prefix + '.' : '') + name;
330
var fullnameLower = fullname.toLowerCase()
331
if (fullnameLower.indexOf(object) > -1) {
332
var score = 0;
333
var parts = fullnameLower.split('.');
334
// check for different match types: exact matches of full name or
335
// "last name" (i.e. last dotted part)
336
if (fullnameLower == object || parts[parts.length - 1] == object) {
337
score += Scorer.objNameMatch;
338
// matches in last name
339
} else if (parts[parts.length - 1].indexOf(object) > -1) {
340
score += Scorer.objPartialMatch;
341
}
342
var match = objects[prefix][name];
343
var objname = objnames[match[1]][2];
344
var title = titles[match[0]];
345
// If more than one term searched for, we require other words to be
346
// found in the name/title/description
347
if (otherterms.length > 0) {
348
var haystack = (prefix + ' ' + name + ' ' +
349
objname + ' ' + title).toLowerCase();
350
var allfound = true;
351
for (i = 0; i < otherterms.length; i++) {
352
if (haystack.indexOf(otherterms[i]) == -1) {
353
allfound = false;
354
break;
355
}
356
}
357
if (!allfound) {
358
continue;
359
}
360
}
361
var descr = objname + _(', in ') + title;
362
363
var anchor = match[3];
364
if (anchor === '')
365
anchor = fullname;
366
else if (anchor == '-')
367
anchor = objnames[match[1]][1] + '-' + fullname;
368
// add custom score for some objects according to scorer
369
if (Scorer.objPrio.hasOwnProperty(match[2])) {
370
score += Scorer.objPrio[match[2]];
371
} else {
372
score += Scorer.objPrioDefault;
373
}
374
results.push([docnames[match[0]], fullname, '#'+anchor, descr, score, filenames[match[0]]]);
375
}
376
}
377
}
378
379
return results;
380
},
381
382
/**
383
* See https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Regular_Expressions
384
*/
385
escapeRegExp : function(string) {
386
return string.replace(/[.*+\-?^${}()|[\]\\]/g, '\\$&'); // $& means the whole matched string
387
},
388
389
/**
390
* search for full-text terms in the index
391
*/
392
performTermsSearch : function(searchterms, excluded, terms, titleterms) {
393
var docnames = this._index.docnames;
394
var filenames = this._index.filenames;
395
var titles = this._index.titles;
396
397
var i, j, file;
398
var fileMap = {};
399
var scoreMap = {};
400
var results = [];
401
402
// perform the search on the required terms
403
for (i = 0; i < searchterms.length; i++) {
404
var word = searchterms[i];
405
var files = [];
406
var _o = [
407
{files: terms[word], score: Scorer.term},
408
{files: titleterms[word], score: Scorer.title}
409
];
410
// add support for partial matches
411
if (word.length > 2) {
412
var word_regex = this.escapeRegExp(word);
413
for (var w in terms) {
414
if (w.match(word_regex) && !terms[word]) {
415
_o.push({files: terms[w], score: Scorer.partialTerm})
416
}
417
}
418
for (var w in titleterms) {
419
if (w.match(word_regex) && !titleterms[word]) {
420
_o.push({files: titleterms[w], score: Scorer.partialTitle})
421
}
422
}
423
}
424
425
// no match but word was a required one
426
if ($u.every(_o, function(o){return o.files === undefined;})) {
427
break;
428
}
429
// found search word in contents
430
$u.each(_o, function(o) {
431
var _files = o.files;
432
if (_files === undefined)
433
return
434
435
if (_files.length === undefined)
436
_files = [_files];
437
files = files.concat(_files);
438
439
// set score for the word in each file to Scorer.term
440
for (j = 0; j < _files.length; j++) {
441
file = _files[j];
442
if (!(file in scoreMap))
443
scoreMap[file] = {};
444
scoreMap[file][word] = o.score;
445
}
446
});
447
448
// create the mapping
449
for (j = 0; j < files.length; j++) {
450
file = files[j];
451
if (file in fileMap && fileMap[file].indexOf(word) === -1)
452
fileMap[file].push(word);
453
else
454
fileMap[file] = [word];
455
}
456
}
457
458
// now check if the files don't contain excluded terms
459
for (file in fileMap) {
460
var valid = true;
461
462
// check if all requirements are matched
463
var filteredTermCount = // as search terms with length < 3 are discarded: ignore
464
searchterms.filter(function(term){return term.length > 2}).length
465
if (
466
fileMap[file].length != searchterms.length &&
467
fileMap[file].length != filteredTermCount
468
) continue;
469
470
// ensure that none of the excluded terms is in the search result
471
for (i = 0; i < excluded.length; i++) {
472
if (terms[excluded[i]] == file ||
473
titleterms[excluded[i]] == file ||
474
$u.contains(terms[excluded[i]] || [], file) ||
475
$u.contains(titleterms[excluded[i]] || [], file)) {
476
valid = false;
477
break;
478
}
479
}
480
481
// if we have still a valid result we can add it to the result list
482
if (valid) {
483
// select one (max) score for the file.
484
// for better ranking, we should calculate ranking by using words statistics like basic tf-idf...
485
var score = $u.max($u.map(fileMap[file], function(w){return scoreMap[file][w]}));
486
results.push([docnames[file], titles[file], '', null, score, filenames[file]]);
487
}
488
}
489
return results;
490
},
491
492
/**
493
* helper function to return a node containing the
494
* search summary for a given text. keywords is a list
495
* of stemmed words, hlwords is the list of normal, unstemmed
496
* words. the first one is used to find the occurrence, the
497
* latter for highlighting it.
498
*/
499
makeSearchSummary : function(htmlText, keywords, hlwords) {
500
var text = Search.htmlToText(htmlText);
501
var textLower = text.toLowerCase();
502
var start = 0;
503
$.each(keywords, function() {
504
var i = textLower.indexOf(this.toLowerCase());
505
if (i > -1)
506
start = i;
507
});
508
start = Math.max(start - 120, 0);
509
var excerpt = ((start > 0) ? '...' : '') +
510
$.trim(text.substr(start, 240)) +
511
((start + 240 - text.length) ? '...' : '');
512
var rv = $('<p class="context"></p>').text(excerpt);
513
$.each(hlwords, function() {
514
rv = rv.highlightText(this, 'highlighted');
515
});
516
return rv;
517
}
518
};
519
520
$(document).ready(function() {
521
Search.init();
522
});
523
524