leanprover / vscode-lean4

Visual Studio Code extension for the Lean 4 proof assistant
Apache License 2.0
158 stars 48 forks source link

fix: filter menu button collapsing goal state #511

Closed mhuisi closed 1 month ago

mhuisi commented 2 months ago

Closes #505.

Vtec234 commented 2 months ago

As far as I can tell, the underlying issue is not really about native vs synthetic React events (BTW, do you have a source for docs about this?). It is more simply that there were a couple of places where we call stopPropagation but not preventDefault. This means that handlers higher up do not get called, but the default event behaviours still occur. You can see it in this example app:

export default function App() {
  return (
    <details>
      <summary onClick={e => e.preventDefault()}>
        <a onClick={e => e.stopPropagation()}>EFFECT</a>
        <span> - </span>
        <a>NO EFFECT</a>
      </summary>
      Content
    </details>
  )
}

So, I propose an alternative fix where we make sure that whenever stopPropagation is called, so is preventDefault. I made this change systematically, and it seems to work (but more testing would be good). I also changed the semantics of Details a bit to inject the <summary> because we should really install the onClick handler there rather than on <details>. I pushed the changes here, but feel free to revert if something is not working.

mhuisi commented 2 months ago

I'm okay with you taking over this PR. Please proceed as you see fit. Your changes look good to me but I haven't tested them in detail.

BTW, do you have a source for docs about this?

https://stackoverflow.com/questions/52444941/when-does-react-create-syntheticevents (and several others, though I can't find documentation of it in the React docs).

I agree that this is due to a lack of preventDefault and not a native browser event firing - I had a misconception about the way the <details> toggle works here and how preventDefault and stopPropagation interact. I think my version worked because it uses a native browser event to call preventDefault and is hence not stopped by the stopPropagation calls in the synthetic events that we use everywhere else.