Hover help for 'obtain' sometimes fail

[anders-was-here]

Hovering help for 'obtain' tactic unexpectedly fail in one of the two example lemmas in the same window. Tested in Firefox and Chromium.

import Mathlib.Data.Complex.Basic

example (a b a' b' : ℂ) (h : (fun z => a * z + b) = fun z => a' * z + b') : a = a' := by
apply congr_fun at h
obtain rfl: b = b' := by  -- Hovering over obtain unexpectedly displays "x✝ : b = b'"
  specialize h 0
  simp at h; exact h

specialize h 1
simp at h
exact h

example (a: Prop) : a -> a := by

obtain h: 3 = 3 -- Hovering over obtain displays useful help "The obtain tactic is a combination..."

admit 

https://live.lean-lang.org/#code=import%20Mathlib.Data.Complex.Basic%0A%0Aexample%20(a%20b%20a'%20b'%20%3A%20%E2%84%82)%20(h%20%3A%20(fun%20z%20%3D%3E%20a%20*%20z%20%2B%20b)%20%3D%20fun%20z%20%3D%3E%20a'%20*%20z%20%2B%20b')%20%3A%20a%20%3D%20a'%20%3A%3D%20by%0Aapply%20congr_fun%20at%20h%0Aobtain%20rfl%3A%20b%20%3D%20b'%20%3A%3D%20by%20%20--%20Hovering%20over%20obtain%20unexpectedly%20displays%20%22x%E2%9C%9D%20%3A%20b%20%3D%20b'%22%0A%20%20specialize%20h%200%0A%20%20simp%20at%20h%3B%20exact%20h%0A%0Aspecialize%20h%201%0Asimp%20at%20h%0Aexact%20h%0A%0Aexample%20(a%3A%20Prop)%20%3A%20a%20-%3E%20a%20%3A%3D%20by%0A%0Aobtain%20h%3A%203%20%3D%203%20--%20Hovering%20over%20obtain%20displays%20useful%20help%20%22The%20obtain%20tactic%20is%20a%20combination...%22%0A%0Aadmit%20

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Stuck.20on.20fun.20in.20hypothesis

[anders-was-here]

But the example abover produces the same hover issue in Visual Studio, so the root cause is likely somewhere else.

[joneugster]

Lean4web does copy most of the code from the "vscode-lean4" extension, although it hasnt been updated for ages. If the error appears in VScode , too. it would be useful tonfogure out if its a problem in the extension or somewhere in core even, and fix it there first.

[anders-was-here]

One small thing, it seems to be the := symbol that kills the hoover text. Here is a smaller example, without import.

example  : True := by
obtain h: True := by  -- Hovering over obtain unexpectedly displays "True"
admit 

example (a: Prop) : a -> a := by
obtain h: 3 = 3 -- Hovering over obtain displays useful help "The obtain tactic is a combination..."
admit