diff options
| author | bob <bcz@cs.brown.edu> | 2019-12-16 10:40:45 -0500 |
|---|---|---|
| committer | bob <bcz@cs.brown.edu> | 2019-12-16 10:40:45 -0500 |
| commit | 9c3acfbd6ad518cd1afcc05a521480d93c07f13a (patch) | |
| tree | a6c6bbbfc2250e7c6d1f1d4b9757e55128597edf /src/client/util/SearchUtil.ts | |
| parent | 7584c5bed0de45f2f656fb289ff67463fb1958ef (diff) | |
| parent | 001cea83f6c57914e0e76a75a94f3e06e542a419 (diff) | |
Merge branch 'master' of https://github.com/browngraphicslab/Dash-Web
Diffstat (limited to 'src/client/util/SearchUtil.ts')
| -rw-r--r-- | src/client/util/SearchUtil.ts | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/client/util/SearchUtil.ts b/src/client/util/SearchUtil.ts index 7a9176bec..1fda82880 100644 --- a/src/client/util/SearchUtil.ts +++ b/src/client/util/SearchUtil.ts @@ -64,7 +64,7 @@ export namespace SearchUtil { const textDocs = newIds.map((id: string) => textDocMap[id]).map(doc => doc as Doc); for (let i = 0; i < textDocs.length; i++) { const testDoc = textDocs[i]; - if (testDoc instanceof Doc && testDoc.type !== DocumentType.KVP && theDocs.findIndex(d => Doc.AreProtosEqual(d, testDoc)) === -1) { + if (testDoc instanceof Doc && testDoc.type !== DocumentType.KVP && testDoc.type !== DocumentType.EXTENSION && theDocs.findIndex(d => Doc.AreProtosEqual(d, testDoc)) === -1) { theDocs.push(Doc.GetProto(testDoc)); theLines.push(newLines[i].map(line => line.replace(query, query.toUpperCase()))); } @@ -74,7 +74,7 @@ export namespace SearchUtil { const docs = ids.map((id: string) => docMap[id]).map(doc => doc as Doc); for (let i = 0; i < ids.length; i++) { const testDoc = docs[i]; - if (testDoc instanceof Doc && testDoc.type !== DocumentType.KVP && (options.allowAliases || theDocs.findIndex(d => Doc.AreProtosEqual(d, testDoc)) === -1)) { + if (testDoc instanceof Doc && testDoc.type !== DocumentType.KVP && testDoc.type !== DocumentType.EXTENSION && (options.allowAliases || theDocs.findIndex(d => Doc.AreProtosEqual(d, testDoc)) === -1)) { theDocs.push(testDoc); theLines.push([]); } |