Introduction chapter: #assertType example likely not behaving as expected in Lean 4.17

[philnguyen]

I tried the example as below:

import Lean

elab "#assertType " termStx:term " : " typeStx:term : command =>
  open Lean Lean.Elab Command Term in
  liftTermElabM
    try
      let tp ← elabType typeStx
      discard $ elabTermEnsuringType termStx tp
      synthesizeSyntheticMVarsNoPostponing
      logInfo "success"
    catch | _ => throwError "failure"

/-- info: success -/
#assertType 5 : Nat

-- don't display names of metavariables
set_option pp.mvars false in

/--
error: type mismatch
  []
has type
  List ?_ : Type _
but is expected to have type
  Nat : Type
-/
#assertType [] : Nat

And could reproduce the following problems either in the online editor, or locally on emacs:

• At the end of the -/ closing block comment, I get error message "unexpected token '#assertType'..."
• If I delete the block comments, the first example #assertType 5 : Nat works as expected. But in the second example, even though I see an error below [] as expected, the entire command is still underlined blue, saying "success" when I hover over it.

I guess Lean has recently changed behaviors that made the examples outdated?

Thanks!