Skip to content

Commit 81e9ee7

Browse files
ofSingularMindofSingularMind
committed
feat: add GraphPPL and ReactiveMP search results. Also add n of N search truncation specification
1 parent b1ed4e4 commit 81e9ee7

1 file changed

Lines changed: 127 additions & 105 deletions

File tree

‎docs/src/assets/header.js‎

Lines changed: 127 additions & 105 deletions
Original file line numberDiff line numberDiff line change
@@ -109,144 +109,166 @@ window.onload = function() {
109109
}
110110

111111
document.addEventListener('DOMContentLoaded', function() {
112-
// === Cross-site search: also search docs.rxinfer.com ===
112+
// === Cross-site search across external docs ===
113113
(function () {
114-
const REMOTE_BASE = 'https://docs.rxinfer.com/stable';
115-
const REMOTE_LABEL = 'Documentation';
116-
let remoteIndex = null;
117-
let remoteIndexPromise = null;
118-
119-
async function fetchRemoteIndex() {
120-
if (remoteIndex !== null) return;
121-
if (remoteIndexPromise) return remoteIndexPromise;
122-
123-
remoteIndexPromise = (async () => {
114+
const REMOTE_SOURCES = [
115+
{ base: 'https://docs.rxinfer.com/stable', label: 'RxInfer Docs', index: null, promise: null },
116+
{ base: 'https://reactivebayes.github.io/ReactiveMP.jl/stable', label: 'ReactiveMP Docs', index: null, promise: null },
117+
{ base: 'https://reactivebayes.github.io/GraphPPL.jl/stable', label: 'GraphPPL Docs', index: null, promise: null },
118+
];
119+
120+
function esc(s) {
121+
return (s || '').replace(/[&<>"']/g, c =>
122+
({ '&': '&amp;', '<': '&lt;', '>': '&gt;', '"': '&quot;', "'": '&#39;' }[c]));
123+
}
124+
125+
async function fetchRemoteIndex(source) {
126+
if (source.index !== null) return;
127+
if (source.promise) return source.promise;
128+
129+
source.promise = (async () => {
124130
try {
125-
const res = await fetch(REMOTE_BASE + '/search_index.js');
131+
const res = await fetch(source.base.replace(/\/+$/, '') + '/search_index.js');
126132
if (!res.ok) return;
127133
const text = await res.text();
128134
const start = text.indexOf('{');
129135
const end = text.lastIndexOf('}');
130136
if (start < 0 || end < start) throw new Error('Invalid format');
131-
remoteIndex = JSON.parse(text.slice(start, end + 1)).docs || [];
137+
source.index = JSON.parse(text.slice(start, end + 1)).docs || [];
132138
} catch (e) {
133-
remoteIndex = [];
139+
source.index = [];
134140
}
135141
})();
136-
137-
return remoteIndexPromise;
142+
143+
return source.promise;
138144
}
139145

140-
function searchRemote(query) {
141-
if (!remoteIndex || !remoteIndex.length) return [];
142-
const words = query.trim().toLowerCase().split(/\s+/).filter(w => w.length > 1);
143-
if (!words.length) return [];
144-
return remoteIndex.filter(doc => {
145-
const hay = (doc.title + ' ' + doc.text).toLowerCase();
146-
return words.every(w => hay.includes(w));
147-
}).slice(0, 8);
148-
}
146+
async function fetchAllRemoteIndices() {
147+
await Promise.all(REMOTE_SOURCES.map(fetchRemoteIndex));
148+
}
149149

150-
function esc(s) {
151-
return (s || '').replace(/[&<>"']/g, c =>
152-
({'&':'&amp;','<':'&lt;','>':'&gt;','"':'&quot;',"'":'&#39;'}[c]));
153-
}
150+
function searchRemote(source, query) {
151+
if (!source.index || !source.index.length) return [];
152+
const words = query.trim().toLowerCase().split(/\s+/).filter(w => w.length > 1);
153+
if (!words.length) return [];
154+
return source.index.filter(doc => {
155+
const hay = (doc.title + ' ' + doc.text).toLowerCase();
156+
return words.every(w => hay.includes(w));
157+
});
158+
}
154159

155-
function extractSnippet(text, query, contextLength = 80) {
156-
const words = query.trim().toLowerCase().split(/\s+/).filter(w => w.length > 1);
157-
if (!words.length || !text) return '';
158-
159-
const lowerText = text.toLowerCase();
160-
161-
// Find first occurrence of any search term
162-
let firstMatchIdx = -1;
163-
for (const word of words) {
164-
const idx = lowerText.indexOf(word);
165-
if (idx !== -1 && (firstMatchIdx === -1 || idx < firstMatchIdx)) {
166-
firstMatchIdx = idx;
160+
function extractSnippet(text, query, contextLength = 80) {
161+
const words = query.trim().toLowerCase().split(/\s+/).filter(w => w.length > 1);
162+
if (!words.length || !text) return '';
163+
164+
const lowerText = text.toLowerCase();
165+
let firstMatchIdx = -1;
166+
for (const word of words) {
167+
const idx = lowerText.indexOf(word);
168+
if (idx !== -1 && (firstMatchIdx === -1 || idx < firstMatchIdx)) {
169+
firstMatchIdx = idx;
170+
}
167171
}
172+
173+
if (firstMatchIdx === -1) return '';
174+
175+
const start = Math.max(0, firstMatchIdx - contextLength);
176+
const end = Math.min(text.length, firstMatchIdx + contextLength);
177+
let snippet = text.slice(start, end);
178+
if (start > 0) snippet = '…' + snippet;
179+
if (end < text.length) snippet = snippet + '…';
180+
181+
for (const word of words) {
182+
const regex = new RegExp(`(${word.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')})`, 'gi');
183+
snippet = snippet.replace(regex, '<mark style="background-color:var(--mark-bg,#fff3cd);padding:0 2px">$1</mark>');
184+
}
185+
186+
return snippet;
168187
}
169-
170-
if (firstMatchIdx === -1) return '';
171-
172-
// Extract context around the match
173-
const start = Math.max(0, firstMatchIdx - contextLength);
174-
const end = Math.min(text.length, firstMatchIdx + contextLength);
175-
let snippet = text.slice(start, end);
176-
177-
// Add ellipsis
178-
if (start > 0) snippet = '…' + snippet;
179-
if (end < text.length) snippet = snippet + '…';
180-
181-
// Highlight all matching words
182-
for (const word of words) {
183-
const regex = new RegExp(`(${word.replace(/[.*+?^${}()|[\]\\]/g, '\\$&')})`, 'gi');
184-
snippet = snippet.replace(regex, '<mark style="background-color:var(--mark-bg,#fff3cd);padding:0 2px">$1</mark>');
185-
}
186-
187-
return snippet;
188-
}
189188

190-
function renderResults(results, query) {
191-
const items = results.map(doc => {
192-
const snippet = extractSnippet(doc.text, query, 80);
193-
return `
194-
<a href="${REMOTE_BASE}/${doc.location || ''}" class="search-result-link w-100 is-flex is-flex-direction-column gap-2 px-4 py-2">
189+
function renderSourceResults(source, results, totalCount, query) {
190+
const items = results.map(doc => {
191+
const snippet = extractSnippet(doc.text, query, 80);
192+
return `
193+
<a href="${source.base.replace(/\/+$/, '')}/${doc.location || ''}" class="search-result-link w-100 is-flex is-flex-direction-column gap-2 px-4 py-2">
195194
<div class="w-100 is-flex is-flex-wrap-wrap is-justify-content-space-between is-align-items-flex-start">
196195
<div class="search-result-title has-text-weight-bold">${esc(doc.title)}</div>
197196
<div class="property-search-result-badge">${esc(doc.category)}</div>
198197
</div>
199198
${snippet ? `<div style="font-size:smaller;opacity:0.8;line-height:1.5">${snippet}</div>` : ''}
200199
<div class="has-text-left" style="font-size:smaller;opacity:0.7">
201-
<i class="fas fa-external-link-alt"></i> ${REMOTE_LABEL}: ${esc((doc.location||'').slice(0,60))}
200+
<i class="fas fa-external-link-alt"></i> ${source.label}: ${esc((doc.location || '').slice(0, 60))}
202201
</div>
203202
</a>
204203
<div class="search-divider w-100"></div>`;
205-
}).join('');
204+
}).join('');
206205

207-
return `<div id="cross-site-results" class="w-100 is-flex is-flex-direction-column gap-2">
206+
const countText = totalCount > results.length
207+
? `${results.length} of ${totalCount} results`
208+
: `${results.length} result${results.length !== 1 ? 's' : ''}`;
209+
210+
return `
208211
<div style="padding:0.5rem 1rem;border-top:1px solid var(--card-border-color,#e9ecef);margin-top:0.5rem">
209-
<span class="is-size-7" style="opacity:0.7">Also from <strong>${REMOTE_LABEL}</strong> — ${results.length} result${results.length !== 1 ? 's' : ''}</span>
210-
</div>${items}</div>`;
211-
}
212+
<span class="is-size-7" style="opacity:0.7">Also from <strong>${source.label}</strong> — ${countText}</span>
213+
</div>
214+
${items}`;
215+
}
216+
217+
function renderResults(sections, query) {
218+
const html = sections.map(section =>
219+
renderSourceResults(section.source, section.results, section.totalCount, query)
220+
).join('');
221+
return `<div id="cross-site-results" class="w-100 is-flex is-flex-direction-column gap-2">${html}</div>`;
222+
}
212223

213224
let injecting = false;
214225

215-
function inject() {
216-
if (injecting) return;
217-
const body = document.querySelector('.search-modal-card-body');
218-
const input = document.querySelector('.documenter-search-input');
219-
if (!body || !input || body.querySelector('#cross-site-results')) return;
220-
221-
if (remoteIndex === null) {
222-
fetchRemoteIndex().then(() => setTimeout(inject, 0));
223-
return;
224-
}
225-
226-
const query = input.value || '';
227-
if (query.trim().length < 2) return;
228-
const results = searchRemote(query);
229-
if (!results.length) return;
230-
injecting = true;
231-
body.insertAdjacentHTML('beforeend', renderResults(results, query));
232-
injecting = false;
233-
}
226+
function inject() {
227+
if (injecting) return;
228+
const body = document.querySelector('.search-modal-card-body');
229+
const input = document.querySelector('.documenter-search-input');
230+
if (!body || !input || body.querySelector('#cross-site-results')) return;
234231

235-
let bodyObserver = null;
236-
function connectBodyObserver() {
237-
const body = document.querySelector('.search-modal-card-body');
238-
if (!body || bodyObserver) return;
239-
bodyObserver = new MutationObserver(() => { if (!injecting) setTimeout(inject, 30); });
240-
bodyObserver.observe(body, { childList: true });
241-
}
232+
if (REMOTE_SOURCES.some(source => source.index === null)) {
233+
fetchAllRemoteIndices().then(() => setTimeout(inject, 0));
234+
return;
235+
}
236+
237+
const query = input.value || '';
238+
if (query.trim().length < 2) return;
239+
240+
const sections = REMOTE_SOURCES.map(source => {
241+
const fullResults = searchRemote(source, query);
242+
return {
243+
source,
244+
totalCount: fullResults.length,
245+
results: fullResults.slice(0, 8),
246+
};
247+
}).filter(section => section.totalCount > 0);
248+
249+
if (!sections.length) return;
242250

243-
new MutationObserver(() => {
244-
const modal = document.getElementById('search-modal');
245-
if (modal) {
246-
if (modal.classList.contains('is-active')) fetchRemoteIndex();
247-
connectBodyObserver();
251+
injecting = true;
252+
body.insertAdjacentHTML('beforeend', renderResults(sections, query));
253+
injecting = false;
248254
}
249-
}).observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['class'] });
250-
fetchRemoteIndex();
255+
256+
let bodyObserver = null;
257+
function connectBodyObserver() {
258+
const body = document.querySelector('.search-modal-card-body');
259+
if (!body || bodyObserver) return;
260+
bodyObserver = new MutationObserver(() => { if (!injecting) setTimeout(inject, 30); });
261+
bodyObserver.observe(body, { childList: true });
262+
}
263+
264+
new MutationObserver(() => {
265+
const modal = document.getElementById('search-modal');
266+
if (modal) {
267+
if (modal.classList.contains('is-active')) fetchAllRemoteIndices();
268+
connectBodyObserver();
269+
}
270+
}).observe(document.body, { childList: true, subtree: true, attributes: true, attributeFilter: ['class'] });
271+
272+
fetchAllRemoteIndices();
251273
})();
252274
});

0 commit comments

Comments
 (0)