Skip to content

Commit 75088c2

Browse files
committed
Migrated FilterInputField.js.js component with JS2TS
1 parent 62d37b5 commit 75088c2

File tree

2 files changed

+74
-68
lines changed

2 files changed

+74
-68
lines changed

benchexec/tablegenerator/react-table/src/components/Table/FilterInputField.js

Lines changed: 0 additions & 68 deletions
This file was deleted.
Lines changed: 74 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,74 @@
1+
// This file is part of BenchExec, a framework for reliable benchmarking:
2+
// https://github.com/sosy-lab/benchexec
3+
//
4+
// SPDX-FileCopyrightText: 2019-2020 Dirk Beyer <https://www.sosy-lab.org>
5+
//
6+
// SPDX-License-Identifier: Apache-2.0
7+
8+
import { memo, useEffect, useRef, useState, ChangeEvent } from "react";
9+
10+
interface FilterInputFieldComponentProps {
11+
id: string;
12+
setFilter?: { value: string };
13+
setCustomFilters: (filter: { id: string; value: string }) => void;
14+
disableTaskText: boolean;
15+
focusedFilter: string;
16+
setFocusedFilter: (filterId: string) => void;
17+
}
18+
19+
const FilterInputFieldComponent: React.FC<FilterInputFieldComponentProps> = ({
20+
id,
21+
setFilter,
22+
setCustomFilters,
23+
disableTaskText,
24+
focusedFilter,
25+
setFocusedFilter,
26+
}) => {
27+
const elementId = `${id}_filter`;
28+
const initFilterValue: string = setFilter ? setFilter.value : "";
29+
30+
const ref = useRef<HTMLInputElement | null>(null);
31+
let [typingTimer, setTypingTimer] = useState<NodeJS.Timeout | null>(null);
32+
let [value, setValue] = useState<string>(initFilterValue);
33+
34+
useEffect(() => {
35+
if (focusedFilter === elementId) {
36+
ref.current?.focus();
37+
}
38+
}, [focusedFilter, elementId]);
39+
40+
const textPlaceholder: string =
41+
id === "id" && disableTaskText
42+
? "To edit, please clear task filter in the sidebar"
43+
: "text";
44+
45+
const onChange = (event: ChangeEvent<HTMLInputElement>): void => {
46+
const newValue: string = event.target.value;
47+
setValue(newValue);
48+
if (typingTimer) {
49+
clearTimeout(typingTimer);
50+
}
51+
const timer = setTimeout(() => {
52+
setCustomFilters({ id, value: newValue });
53+
document.getElementById(elementId)?.focus();
54+
}, 500);
55+
setTypingTimer(timer);
56+
};
57+
58+
return (
59+
<input
60+
key={elementId}
61+
id={elementId}
62+
className="filter-field"
63+
placeholder={textPlaceholder}
64+
defaultValue={value}
65+
onChange={onChange}
66+
disabled={id === "id" ? disableTaskText : false}
67+
type="search"
68+
onFocus={() => setFocusedFilter(elementId)}
69+
ref={ref}
70+
/>
71+
);
72+
}
73+
74+
export default memo(FilterInputFieldComponent);

0 commit comments

Comments
 (0)