From bc7533d18f54b57fc8378571cf33501c79eff188 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 28 Feb 2023 14:37:14 +0100 Subject: [PATCH] loading icon for loading goals --- client/src/components/infoview/info.tsx | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 3958b5f..6748bb8 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -16,7 +16,7 @@ import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/ import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' -import { Troubleshoot } from '@mui/icons-material'; +import { CircularProgress } from '@mui/material'; type InfoStatus = 'updating' | 'error' | 'ready'; type InfoKind = 'cursor' | 'pin'; @@ -122,10 +122,12 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { }
- { goals && goals.goals.length > 0 + { goals && ( + goals.goals.length > 0 ? <>
Main Goal
- :
No Goals
} + :
No Goals
+ ) }
{userWidgets.map(widget => @@ -143,7 +145,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { {' '}or { e.preventDefault(); setPaused(false); }}>resume updating {' '}to see information. : -
Loading goal...
)} + <>
Loading goal...
)} {goals && goals.goals.length > 1 &&