Success message

Stream: general

[Patrick Massot]

Is there anyone who can make use of the comment at https://github.com/leanprover-community/mathlib/blob/master/src/tactic/interactive_expr.lean#L402-L408? Copy and pasting those lines seem to do nothing.

[Rob Lewis]

It works for me -- with this I see my_message instead of Goals accomplished! :tada: at the end of the example.

import tactic.interactive_expr

meta def my_new_msg {α : Type} : widget.html α := "my message"
attribute [vm_override my_new_msg] widget_override.goals_accomplished_message

example : true :=
begin
  trivial,
end

[Patrick Massot]

Oh, I had too many layers of overrides.

[Patrick Massot]

Thanks