feat: show message when goals are unfocused

When there are unfocused goals (when bullets are used) we now display
a message stating the subproof is complete but there are still unfocused
goals.

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/templates/ProovViewPage.tsx

@@ -49,12 +49,13 @@ const proofViewPage: FunctionComponent<ProofViewPageProps> = (props) => {
             <VSCodePanelView className={classes.View}> 
                 <GoalSection 
                     key={"goals"}
-                    goals={goals!.main} 
+                    goals={goals!.main}
                     collapseGoalHandler={(id) => collapseGoalHandler(id, ProofViewGoalsKey.main)} 
                     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, but there are some unfocused goals. Focus next goal with bullet -." :
                         "There are no more subgoals"
                     }
                     emptyIcon={

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

@@ -16,6 +16,7 @@ export type ProofViewGoalsType = {
     main: CollapsibleGoal[];
     shelved: CollapsibleGoal[];
     givenUp: CollapsibleGoal[];
+    unfocused: CollapsibleGoal[];
 };
 
 export enum ProofViewGoalsKey {

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;
     }