can widgets run tactics for us?

Stream: general

[Scott Morrison]

I've always been curious what it would be like have library_search run constantly --- I guess anytime that the cursor is at the end of begin end block, I'd like to spin up a library_search, and insert a light bulb if it succeeds and do nothing otherwise.

Is this at all achievable with our current UI? Can I add a widget that calls back to the server to run library_search, and then changes its html appearance if it gets a good result?

[Bryan Gin-ge Chen]

It might be possible but it'd be a bit of a disgusting hack. The only ways I know to get the Lean 3 server to run code involve inserting code into the file it has loaded and then filtering the messages for output. So you could insert a by library_search at the beginning / end of the line that the cursor is on and then remove it after Lean returned the result. (There are hole-commands, too, but you have to have {! !} or _ in the Lean code to be able to trigger those.)

It'd be much nicer if we had a Lean server command for #evaling or run_cmding at a certain point in a file...