Don't show aux obligations, unless they are failed.

Signed-off-by: Karolis Petrauskas <k.petrauskas@gmail.com>
tlaplus · Jan 28, 2024 · 38aa440 · 38aa440
1 parent 234b4b7
commit 38aa440
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 4 deletions.
diff --git a/src/webview/current-proof-step/main.tsx b/src/webview/current-proof-step/main.tsx
@@ -1,6 +1,6 @@
 import * as React from 'react';
 import { createRoot } from 'react-dom/client';
-import { TlapsProofStepDetails } from '../../model/tlaps.ts';
+import { TlapsProofObligationState, TlapsProofStepDetails } from '../../model/tlaps.ts';
 import { Obligation } from './obligation/index.tsx';
 import { StepCounts } from './stepCounts/index.tsx';
 import { VSCodeLink } from '@vscode/webview-ui-toolkit/react/index';
@@ -23,6 +23,16 @@ const CurrentProofStepViewApp = React.memo(({ details }: CurrentProofStepViewApp
                 default: return kind;
             }
         };
+        const obsMain: TlapsProofObligationState[] = [];
+        const obsOthers: TlapsProofObligationState[] = [];
+        details.obligations.forEach(obl => {
+            // We will show the main obligations before the other.
+            if (obl.role === 'main') {
+                obsMain.push(obl);
+            } else {
+                obsOthers.push(obl);
+            }
+        });
         return (
             <React.StrictMode>
                 <section>
@@ -39,9 +49,8 @@ const CurrentProofStepViewApp = React.memo(({ details }: CurrentProofStepViewApp
                     <StepCounts label={subLabel} counts={details.sub_count}></StepCounts>
                 </section>
                 <section>
-                    {details.obligations.map((obl, index) =>
-                        <Obligation key={index} details={details} obligation={obl} />
-                    )}
+                    {obsMain.map((obl, index) => <Obligation key={index} details={details} obligation={obl} />)}
+                    {obsOthers.map((obl, index) => <Obligation key={index} details={details} obligation={obl} />)}
                 </section>
             </React.StrictMode>
         );

diff --git a/src/webview/current-proof-step/obligation/index.tsx b/src/webview/current-proof-step/obligation/index.tsx
@@ -8,6 +8,10 @@ import './index.css';
 
 interface ObligationI { details: TlapsProofStepDetails; obligation: TlapsProofObligationState }
 export const Obligation = React.memo(({ details, obligation }: ObligationI) => {
+    if (obligation.role === 'aux' && obligation.status !== 'failed') {
+        // Do not show the auxiliary obligations, unless they are failed.
+        return null;
+    }
     const location = { uri: details.location.uri, range: obligation.range } as Location;
     const showLocation = () => vscodeClient.showLocation(location);
     const results = obligation.results && obligation.results.length > 0