use GoalsTab in editor mode

client/src/components/infoview/info.tsx

@@ -17,6 +17,7 @@ import { goalsToString, Goal, MainAssumptions, OtherGoals } from './goals'
 import { InteractiveTermGoal, InteractiveGoalsWithHints, InteractiveGoals, ProofState } from './rpc_api'
 import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from '../../state/context'
 import { useTranslation } from 'react-i18next'
+import { GoalsTabs } from './main'
 
 // TODO: All about pinning could probably be removed
 type InfoKind = 'cursor' | 'pin'
@@ -123,37 +124,39 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 Error updating:{' '}{error}.
                 <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a>
             </div>}
+        <AllMessages /> {/* TODO: Move error messages to Chat instead */}
         <LocationsContext.Provider value={locs}>
           <div className="goals-section">
+
             { goals &&  goals.goals.length > 0 && <>
-              <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
+              <GoalsTabs goals={goals.goals.map(goal => ({goal: goal, hints: []}))} last={false} onClick={() => {}} onGoalChange={() => {}}/>
-              <OtherGoals filter={goalFilter} goals={goals.goals} />
+              {/* <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
+              <OtherGoals filter={goalFilter} goals={goals.goals} /> */}
             </>}
           </div>
-          <div>
+          {/* <div>
             { goals && (goals.goals.length > 0
               ? <Goal typewriter={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
               : <div className="goals-section-title">{t("No Goals")}</div>
             )}
-          </div>
+          </div> */}
         </LocationsContext.Provider>
-        {userWidgets.map(widget =>
+        {/* {userWidgets.map(widget =>
           <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
             <summary className='mv2 pointer'>{widget.name}</summary>
             <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []}
               termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
           </details>
-        )}
+        )} */}
-        {nothingToShow && (
+        {/* {nothingToShow && (
             isPaused ?
-                /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
+                /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 * /
                 <span>Updating is paused.{' '}
                     <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a>
                     {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
                     {' '}to see information.
                 </span> :
-                <><CircularProgress /><div>{t("Loading goal…")}</div></>)}
+                <><CircularProgress /><div>{t("Loading goal…")}</div></>)} */}
-        <AllMessages />
         {/* <LocationsContext.Provider value={locs}>
             {goals && goals.goals.length > 1 && <div className="goals-section other-goals">
                     <div className="goals-section-title">Weitere Goals</div>

client/src/components/infoview/main.tsx

@@ -29,7 +29,7 @@ import { ChatContext, PageContext, PreferencesContext, MonacoEditorContext, Proo
 import { Typewriter, getInteractiveDiagsAt, hasErrors, hasInteractiveErrors } from './typewriter';
 import { InteractiveDiagnostic } from '@leanprover/infoview/*';
 import { CircularProgress } from '@mui/material';
-import { GameHint, InteractiveGoalsWithHints, ProofState } from './rpc_api';
+import { GameHint, InteractiveGoalWithHints, InteractiveGoalsWithHints, ProofState } from './rpc_api';
 import { store } from '../../state/store';
 import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { DiagnosticSeverity } from 'vscode-languageclient';
@@ -340,17 +340,17 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
 // }, fastIsEqual)
 
 /** The tabs of goals that lean has after the command of this step has been processed */
-function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
+export function GoalsTabs({ goals, last, onClick, onGoalChange=(n)=>{}}: { goals: InteractiveGoalWithHints[], last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
   let { t } = useTranslation()
   const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
 
-  if (proofStep.goals.length == 0) {
+  if (goals.length == 0) {
     return <></>
   }
 
   return <div className="goal-tabs" onClick={onClick}>
     <div className={`tab-bar ${last ? 'current' : ''}`}>
-      {proofStep.goals.map((goal, i) => (
+      {goals.map((goal, i) => (
         // TODO: Should not use index as key.
         <div key={`proof-goal-${i}`} className={`tab ${i == (selectedGoal) ? "active" : ""}`} onClick={(ev) => { onGoalChange(i); setSelectedGoal(i); ev.stopPropagation() }}>
           {i ? t("Goal") + ` ${i + 1}` : t("Active Goal")}
@@ -358,7 +358,7 @@ function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofSte
       ))}
     </div>
     <div className="goal-tab vscode-light">
-      <Goal typewriter={false} filter={goalFilter} goal={proofStep.goals[selectedGoal]?.goal} unbundle={false} />
+      <Goal typewriter={false} filter={goalFilter} goal={goals[selectedGoal]?.goal} unbundle={false} />
     </div>
   </div>
 }
@@ -570,7 +570,7 @@ export function TypewriterInterface({props}) {
                   }
                   {/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
                   {!(isLastStepWithErrors(proof, i)) &&
-                    <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
+                    <GoalsTabs goals={step.goals} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
                   }
                   {mobile && i == proof?.steps.length - 1 &&
                     <MoreHelpButton />

client/src/css/infoview.css

@@ -91,8 +91,8 @@
   flex-direction: row;
 }
 
-.goals-section div {
+.goal-tabs {
-  flex-grow: 1;
+  width: 100%;
 }
 
 #current-proof, #main-assumptions {