Merge pull request #901 from coq-community/bullet

feat: show message when goals are unfocused

client/goal-view-ui/src/App.tsx

@@ -35,8 +35,11 @@ const app = () => {
                     shelved: allGoals.shelvedGoals.map((goal: Goal) => {
                         return {...goal, isOpen: true};
                     }),
-                    givenUp: allGoals.givenUpGoals.map((goal: Goal, index: number) => {
+                    givenUp: allGoals.givenUpGoals.map((goal: Goal) => {
                         return {...goal, isOpen: true}; 
+                    }),
+                    unfocused: allGoals.unfocusedGoals.map((goal: Goal) => {
+                        return {...goal, isOpen: false};
                     })
                 }
             );

client/goal-view-ui/src/components/atoms/EmptyState.module.css

@@ -1,7 +1,6 @@
 .EmptyStateSection {
     display: flex;
     flex-direction: row;
-    justify-content: space-between;
     align-items: flex-start;
     align-content: center;
 }

client/goal-view-ui/src/components/organisms/GoalSection.module.css

@@ -0,0 +1,12 @@
+.UnfocusedView {
+    display: flex;
+    flex-direction: column;
+    width: 100%;
+}
+
+.HintText {
+    font-style: italic;
+    font-family: var(--vscode-editor-fonont-family);
+    font-size: small;
+    opacity: 0.5;
+}

client/goal-view-ui/src/components/organisms/GoalSection.tsx

@@ -1,25 +1,26 @@
-import React, {FunctionComponent, ReactNode, useEffect, useRef, useState} from 'react';
-import { VscPass } from 'react-icons/vsc';
+import React, {FunctionComponent, useEffect, useRef} from 'react';
 
 import GoalCollapsibleSection from './GoalCollapsibles';
 import GoalTabSection from './GoalTabs';
 import EmptyState from '../atoms/EmptyState';
 import { CollapsibleGoal } from '../../types';
 
+import classes from './GoalSection.module.css';
 
 type GoalSectionProps = {
     goals: CollapsibleGoal[],
     collapseGoalHandler: (id: string) => void, 
     displaySetting: string;
     emptyMessage: string;
     emptyIcon?: JSX.Element;
+    unfocusedGoals?: CollapsibleGoal[],
     maxDepth: number;
     helpMessageHandler: (message: string) => void;
 };
 
 const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
 
-    const {goals, collapseGoalHandler, displaySetting, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
+    const {goals, collapseGoalHandler, displaySetting, unfocusedGoals, emptyMessage, emptyIcon, maxDepth, helpMessageHandler} = props;
     const emptyMessageRef = useRef<HTMLDivElement>(null);
 
     useEffect(() => {
@@ -38,10 +39,19 @@ const goalSection: FunctionComponent<GoalSectionProps> = (props) => {
     }
 
     const section = goals.length === 0 ?
-        <>
+        unfocusedGoals !== undefined && unfocusedGoals.length > 0 ?
+        <div className={classes.UnfocusedView}>
             <EmptyState message={emptyMessage} icon={emptyIcon} />
+            <div className={classes.HintText}>
+                Next unfocused goals (focus with bullet):
+            </div>
             <div ref={emptyMessageRef}/>
-        </>
+            <GoalCollapsibleSection goals={unfocusedGoals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler} />
+        </div>
+        : <>
+            <EmptyState message={emptyMessage} icon={emptyIcon} />
+            <div ref={emptyMessageRef}/>
+          </>
     : displaySetting === 'Tabs' ?
         <GoalTabSection goals={goals} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>
         : <GoalCollapsibleSection goals={goals} collapseGoalHandler={collapseGoalHandler} maxDepth={maxDepth} helpMessageHandler={helpMessageHandler}/>;

client/goal-view-ui/src/components/templates/ProovViewPage.tsx

@@ -49,12 +49,14 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
             <VSCodePanelView className={classes.View}> 
                 <GoalSection 
                     key={"goals"}
-                    goals={goals!.main} 
-                    collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.main)} 
+                    goals={goals!.main}
+                    unfocusedGoals={goals!.unfocused}
+                    collapseGoalHandler={(id) => collapseGoalHandler(id, goals!.main.length ? ProofViewGoalsKey.main : ProofViewGoalsKey.unfocused)}
                     displaySetting={displaySetting}
                     emptyMessage={
                         goals!.shelved.length ? "There are shelved goals. Try using `Unshelve.`" :
                         goals!.givenUp.length ? "There are some goals you gave up. Go back and solve them, or use `Admitted.`" :
+                        goals!.unfocused.length ? "The subproof is complete." :
                         "There are no more subgoals"
                     }
                     emptyIcon={

client/goal-view-ui/src/types.ts

@@ -16,12 +16,14 @@ export type ProofViewGoalsType = {
     main: CollapsibleGoal[];
     shelved: CollapsibleGoal[];
     givenUp: CollapsibleGoal[];
+    unfocused: CollapsibleGoal[];
 };
 
 export enum ProofViewGoalsKey {
     main = "main", 
     shelved = "shelved", 
-    givenUp = "givenUp"
+    givenUp = "givenUp",
+    unfocused = "unfocused"
 }
 
 export enum MessageSeverity {

client/src/protocol/types.ts

@@ -28,11 +28,6 @@ export type PpString =
   | ["Ppcmd_force_newline"]
   | ["Ppcmd_comment", string[]];
 
-interface Error {
-    code: integer; 
-    message: string; 
-}
-
 export interface Goal {
     id: integer;
     goal: PpString;
@@ -43,6 +38,7 @@ export interface ProofViewGoals {
     goals: Goal[];
     shelvedGoals: Goal[];
     givenUpGoals: Goal[];
+    unfocusedGoals: Goal[];
 }
 
 export enum MessageSeverity {

language-server/protocol/proofState.ml

@@ -26,6 +26,7 @@ type t = {
   goals: goal list;
   shelvedGoals: goal list;
   givenUpGoals: goal list;
+  unfocusedGoals: goal list;
 } [@@deriving yojson]
 
 open Printer
@@ -106,12 +107,15 @@ let get_proof ~previous diff_mode st =
     in
     let env = Global.env () in
     let proof_data = Proof.data proof in
+    let b_goals = Proof.background_subgoals proof in
     let sigma = proof_data.sigma in
     let goals = List.map (mk_goal env sigma) proof_data.goals in
+    let unfocusedGoals = List.map (mk_goal env sigma) b_goals in
     let shelvedGoals = List.map (mk_goal env sigma) (Evd.shelf sigma) in
     let givenUpGoals = List.map (mk_goal env sigma) (Evar.Set.elements @@ Evd.given_up sigma) in
     Some {
       goals;
       shelvedGoals;
       givenUpGoals;
+      unfocusedGoals;
     }