improve command line display

client/src/components/infoview/goals.tsx

@@ -114,6 +114,11 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
     </div>
 }
 
+interface GoalProps2 {
+  goals: InteractiveGoal[]
+  filter: GoalFilterState
+}
+
 interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
@@ -121,6 +126,11 @@ interface GoalProps {
     commandLine: boolean
 }
 
+interface ProofDisplayProps {
+  proof: string
+}
+
+
 /**
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
@@ -154,10 +164,10 @@ export const Goal = React.memo((props: GoalProps) => {
     return <div>
         {/* {goal.userName && <div><strong className="goal-case">case </strong>{goal.userName}</div>} */}
         {filter.reverse && goalLi}
-        { objectHyps.length > 0 &&
+        {! commandLine && objectHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Objekte:</div>
             {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
-        { assumptionHyps.length > 0 &&
+        {!commandLine && assumptionHyps.length > 0 &&
             <div className="hyp-group"><div className="hyp-group-title">Annahmen:</div>
             {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
         {commandLine && commandLineMode && <CommandLine />}
@@ -166,6 +176,79 @@ export const Goal = React.memo((props: GoalProps) => {
     </div>
 })
 
+export const MainAssumptions = React.memo((props: GoalProps2) => {
+  const { goals, filter } = props
+
+  const goal = goals[0]
+  const filteredList = getFilteredHypotheses(goal.hyps, filter);
+  const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
+  const locs = React.useContext(LocationsContext)
+
+  const goalLocs = React.useMemo(() =>
+    locs && goal.mvarId ?
+      { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
+        undefined,
+      [locs, goal.mvarId])
+
+  const goalLi = <div key={'goal'}>
+    <div className="goal-title">Goal: </div>
+    <LocationsContext.Provider value={goalLocs}>
+      <InteractiveCode fmt={goal.type} />
+    </LocationsContext.Provider>
+  </div>
+
+  const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
+  const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
+
+  return <div id="main-assumptions">
+    <div className="goals-section-title">Aktuelles Goal</div>
+    {filter.reverse && goalLi}
+    { objectHyps.length > 0 &&
+      <div className="hyp-group"><div className="hyp-group-title">Objekte:</div>
+      {objectHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}</div> }
+    { assumptionHyps.length > 0 &&
+      <div className="hyp-group">
+        <div className="hyp-group-title">Annahmen:</div>
+        {assumptionHyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
+      </div> }
+  </div>
+})
+
+export const OtherGoals = React.memo((props: GoalProps2) => {
+  const { goals, filter } = props
+  return <>
+    {goals && goals.length > 1 &&
+      <div id="other-goals" className="other-goals">
+        <div className="goals-section-title">Weitere Goals</div>
+        {goals.slice(1).map((goal, i) =>
+          <details key={i}>
+            <summary>
+              <InteractiveCode fmt={goal.type} />
+            </summary>
+            <Goal commandLine={false} filter={filter} goal={goal} />
+          </details>)}
+      </div>}
+  </>
+})
+
+export const ProofDisplay = React.memo((props : ProofDisplayProps) => {
+  const { proof } = props
+  const steps = proof.match(/.+/g)
+  return <>
+    { steps &&
+      <div id="current-proof">
+        <div className="goals-section-title">Bisheriger Beweis</div>
+        <div className="proof-display-wrapper">
+          <div className="proof-display">
+            {steps.map((s) =>
+              <div>{s}</div>
+            )}
+          </div>
+        </div>
+      </div>}
+  </>
+})
+
 interface GoalsProps {
     goals: InteractiveGoals
     filter: GoalFilterState

client/src/components/infoview/info.tsx

@@ -3,7 +3,7 @@
 import * as React from 'react';
 import type { Location, Diagnostic } from 'vscode-languageserver-protocol';
 
-import { goalsToString, Goal, FilteredGoals } from './goals'
+import { goalsToString, Goal, MainAssumptions, OtherGoals, FilteredGoals, ProofDisplay } from './goals'
 import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
     mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util';
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts';
@@ -17,6 +17,8 @@ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-i
 import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation';
 import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode'
 import { CircularProgress } from '@mui/material';
+import { InputModeContext, MonacoEditorContext } from '../Level'
+
 
 type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -84,10 +86,11 @@ interface InfoDisplayContentProps extends PausableProps {
     error?: string;
     userWidgets: UserWidgetInstance[];
     triggerUpdate: () => Promise<void>;
+    proof? : string;
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
-    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused} = props;
+    const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props;
 
     const hasWidget = userWidgets.length > 0;
     const hasError = !!error;
@@ -122,19 +125,24 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             </div>}
         <LocationsContext.Provider value={locs}>
           <div className="goals-section">
-                { goals && (
+            { goals &&  goals.goals.length > 0 && <>
-                    goals.goals.length > 0
+              <MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
-                  ? <><div className="goals-section-title">Aktuelles Goal</div>
+              <ProofDisplay proof={proof}/>
-                    <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} /></>
+              <OtherGoals filter={goalFilter} goals={goals.goals} />
+            </>}
+          </div>
+          <div>
+            { goals && (goals.goals.length > 0
+              ? <Goal commandLine={true} filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
               : <div className="goals-section-title">No Goals</div>
-                ) }
+            )}
           </div>
         </LocationsContext.Provider>
         {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.map (goal => goal) : []} termGoal={termGoal}
+            <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals.map (goal => goal) : []}
-                    selectedLocations={selectedLocs} widget={widget}/>
+              termGoal={termGoal} selectedLocations={selectedLocs} widget={widget}/>
           </details>
         )}
         {nothingToShow && (
@@ -203,12 +211,14 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
         setPaused(isPaused => !isPaused);
     });
 
+    const editor = React.useContext(MonacoEditorContext)
+
     return (
     <RpcContext.Provider value={rpcSess}>
     {/* <details open> */}
         {/* <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} /> */}
         <div>
-            <InfoDisplayContent {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
+            <InfoDisplayContent {...props} proof={editor.getValue()} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         </div>
     {/* </details> */}
     </RpcContext.Provider>

client/src/components/infoview/infoview.css

@@ -79,3 +79,52 @@
 .other-goals .goals-section-title, .other-goals summary, .other-goals summary .font-code {
   color: #5191d1;
 }
+
+.goals-section {
+  display: flex;
+  flex-direction: row;
+}
+
+.goals-section div {
+  flex-grow: 1;
+}
+
+#current-proof, #main-assumptions {
+  margin-right: 0.8em;
+}
+
+#current-proof, #other-goals {
+  margin-left: 0.8em;
+}
+
+.proof-display {
+  max-height: 6em;
+  overflow-y: auto;
+  overscroll-behavior-y: contain;
+  scroll-snap-type: y proximity;
+  color: #ccc;
+
+}
+
+.proof-display div:nth-last-child(4) {
+  color: #999;
+}
+
+.proof-display div:nth-last-child(3) {
+  color: #666;
+}
+
+.proof-display div:nth-last-child(2) {
+  color: #333;
+}
+
+.proof-display div:nth-last-child(1) {
+  color: #000;
+  scroll-snap-align: end;
+}
+
+.proof-display-wrapper {
+  background-color: #f0f0f0;
+  border-radius: 1em;
+  padding: 0.6em;
+}