~cypheon/idris2-quickdocs

12e9ed8c011d39cc68db3cfe2e52a445e68a8122 — Johann Rudloff 2 months ago da9ea60 main
Escape "pipe" character when preparing the search regex
1 files changed, 2 insertions(+), 1 deletions(-)

M app.js
M app.js => app.js +2 -1
@@ 71,7 71,8 @@ function matchSubsequence (item, query) {
}

function matchNamespace (item, query) {
  const quoted = query.replaceAll(/[.+*\\()[\]<>$^]/g, '\\$&');
  // Try to escape any characters that have special meaning in a regex
  const quoted = query.replaceAll(/[.+*\\()[\]<>$|^]/g, '\\$&');
  const reQuery = new RegExp(quoted.replaceAll('\\.', '.*\\.'));
  return reQuery.test(item[IDX_FULLNAME_LOWER]);
}