expand_tactic と expand_command を統一する

[Seasawher]

謎の挙動でうまくいかないです

import Lean

def lxor (l r : Bool) : Bool := !l && r

open Lean

/-- command to expand macro of `command` -/
elab "#expand_command " t:command : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

/-- command to expand macro of `tactic` -/
elab "#expand_tactic " t:tactic : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

/-- syntax category for `#expand` -/
declare_syntax_cat macro_stx
syntax command : macro_stx
syntax tactic : macro_stx

-- this works!
/-- info: notation:50 lhs✝:51 " LXOR " rhs✝:51 => lxor lhs✝ rhs✝ -/
#guard_msgs in
  #expand_command infix:50 " LXOR " => lxor

syntax "#expand" macro_stx : command

-- new command for both tactic and command
elab "#expand " t:macro_stx : command => do
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

-- This does not work....
-- why???
/-
Not a macro
-/
#expand infix:50 " LXOR " => lxor

[spinylobster]

こんな感じで書いたらいけました

elab "#expand " t:macro_stx : command => do
  let t : Syntax := match t.raw with
  | .node _ _ #[t] => t
  | _ => t.raw
  match ← Elab.liftMacroM <| Lean.Macro.expandMacro? t with
  | none => logInfo m!"Not a macro"
  | some t => logInfo m!"{t}"

dbg_trace tで確認したところ、macro_stx_という表示が見えたので「多分元々の値がSyntax.nodeに包まれているんだろうな」と想像してそれを剥がす処理を挟んだ感じです。