message: fix: revert to old message update logic
diff: @@ -86,6 +86,7 @@ interface InfoDisplayProps extends InfoPinnable {
  termGoal?: InteractiveGoal;
  error?: string;
  rpcSess: RpcSession;
  + messagesRpcSess: RpcSession;
  triggerUpdate: () => Promise<void>;
  }
  @@ -104,7 +105,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
  };
  const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>({ reverse: false, isType: true, isInstance: true, isHiddenAssumption: true});
  - const {kind, pos, status, messages, goals, termGoal, error, rpcSess} = props;
  + const {kind, pos, status, messages, goals, termGoal, error, rpcSess, messagesRpcSess} = props;
  const ec = React.useContext(EditorContext);
  let copyGoalToComment: (() => void) | undefined
  @@ -197,6 +198,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
  </div>
  </Details>
  </div>
  + <RpcContext.Provider value={messagesRpcSess}>
  <div style={{display: hasMessages ? 'block' : 'none'}}>
  <Details initiallyOpen>
  <summary className="mv2 pointer">
  @@ -207,6 +209,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
  </div>
  </Details>
  </div>
  + </RpcContext.Provider>
  {nothingToShow && (
  isPaused ?
  /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
  @@ -301,7 +304,7 @@ function InfoAux(props: InfoProps) {
  // We encapsulate `InfoDisplay` props in a single piece of state for atomicity, in particular
  // to avoid displaying a new position before the server has sent us all the goal state there.
  - const mkDisplayProps = () => ({ ...props, messages, pos, goals, termGoal, error, rpcSess });
  + const mkDisplayProps = () => ({ ...props, pos, goals, termGoal, error, rpcSess });
  const [displayProps, setDisplayProps] = React.useState(mkDisplayProps());
  const [shouldUpdateDisplay, setShouldUpdateDisplay] = React.useState(false);
  if (shouldUpdateDisplay) {
  @@ -364,6 +367,7 @@ function InfoAux(props: InfoProps) {
  React.useEffect(() => void triggerUpdate(), [pos.uri, pos.line, pos.character, serverIsProcessing]);
  return (
  - <InfoDisplay {...displayProps} status={status} triggerUpdate={triggerUpdate} />
  + <InfoDisplay {...displayProps} messages={messages} messagesRpcSess={rpcSess}
  + status={status} triggerUpdate={triggerUpdate} />
  );
  }
  