Hole commands

Stream: lean4

[Evgenia Karunus]

1. Do I understand it right that the purpose of hole commands ({! !}, https://leanprover-community.github.io/mathlib_docs/hole_commands.html) is just to provide a nice UI for common commands (linting, performing library_search)? Like CMD+P in text editors?
2. Are there/will there be hole commands in Lean 4? I could make a hole command work in Lean 3 (screenshot attached), but not in Lean 4.
   Lean 3:
   

[Sebastian Ullrich]

@David Thrane Christiansen wrote about the potential purpose of holes, should we re-add them, compared to other features here: https://github.com/leanprover/lean4/issues/1223#issuecomment-1159050274