Fix tab switching and missing key

Signed-off-by: Afonso Fernandes <21228942+afonsonf@users.noreply.github.com>
tlaplus · May 26, 2023 · 314b870 · 314b870
1 parent 0426d38
commit 314b870
Show file tree

Hide file tree

Showing 2 changed files with 20 additions and 10 deletions.
diff --git a/src/webview/check-result-view.tsx b/src/webview/check-result-view.tsx
@@ -4,29 +4,37 @@ import { ErrorTraceSection } from './checkResultView/errorTraceSection';
 import { HeaderSection } from './checkResultView/headerSection';
 import { OutputSection } from './checkResultView/outputSection';
 import { StatsSection } from './checkResultView/statsSection';
+import { vscode } from './checkResultView/vscode';
 
 import '@vscode/codicons/dist/codicon.css';
+import { ModelCheckResult } from '../model/check';
 import './check-result-view.css';
 
 const receiveState = () => {
-    const [state, setState] = React.useState({checkResult: null});
-    window.addEventListener('message', (event) => setState({checkResult: event.data.checkResult}));
-    return state;
+    const [state, setState] = React.useState(vscode.getState());
+
+    window.addEventListener('message',
+        (event) => {
+            setState(event.data.checkResult);
+            vscode.setState(event.data.checkResult);
+        });
+
+    return state as ModelCheckResult;
 };
 
 const CheckResultViewApp = () => {
     const state = receiveState();
 
-    if (state.checkResult === null) {
+    if (!state) {
         return (null);
     }
 
     return (
         <>
-            <HeaderSection checkResult={state.checkResult}/>
-            <StatsSection checkResult={state.checkResult}/>
-            <OutputSection checkResult={state.checkResult}/>
-            <ErrorTraceSection checkResult={state.checkResult}/>
+            <HeaderSection checkResult={state}/>
+            <StatsSection checkResult={state}/>
+            <OutputSection checkResult={state}/>
+            <ErrorTraceSection checkResult={state}/>
         </>
     );
 };

diff --git a/src/webview/checkResultView/statsSection.tsx b/src/webview/checkResultView/statsSection.tsx
@@ -48,7 +48,8 @@ const StatesStats = ({stats}: {stats: InitialStateStatItem[]}) => {
                 value: 'Queue', isNumber: true,
                 tooltip: 'The number of states whose successor states have not been found yet'
             }].map(
-                (v, id) => <DataGridCellHeader id={id+1} value={v.value} isNumber={v.isNumber} tooltip={v.tooltip}/>)}
+                (v, id) =>
+                    <DataGridCellHeader key={id} id={id+1} value={v.value} isNumber={v.isNumber} tooltip={v.tooltip}/>)}
         </VSCodeDataGridRow>
     );
 
@@ -98,7 +99,8 @@ const CoverageStats = ({stats}: {stats: CoverageItem[]}) => {
                 value: 'Distinct', isNumber: true,
                 tooltip: 'Total number of times the action produced a distinct successor state'
             }].map(
-                (v, id) => <DataGridCellHeader id={id+1} value={v.value} isNumber={v.isNumber} tooltip={v.tooltip}/>)}
+                (v, id) =>
+                    <DataGridCellHeader key={id} id={id+1} value={v.value} isNumber={v.isNumber} tooltip={v.tooltip}/>)}
         </VSCodeDataGridRow>
     );