diff --git a/Batteries/Tactic/PrintPrefix.lean b/Batteries/Tactic/PrintPrefix.lean index b83e7b0ad8..dbedad072f 100644 --- a/Batteries/Tactic/PrintPrefix.lean +++ b/Batteries/Tactic/PrintPrefix.lean @@ -108,12 +108,12 @@ by setting `showTypes` to `false`: The complete set of flags can be seen in the documentation for `Lean.Elab.Command.PrintPrefixConfig`. -/ -elab (name := printPrefix) "#print" tk:"prefix" - cfg:(Lean.Parser.Tactic.config)? name:ident : command => liftTermElabM do - let nameId := name.getId - let opts ← elabPrintPrefixConfig (mkOptionalNode cfg) - let mut msgs ← matchingConstants opts nameId - if msgs.isEmpty then - if let [name] ← resolveGlobalConst name then - msgs ← matchingConstants opts name - logInfoAt tk (.joinSep msgs.toList "") +elab (name := printPrefix) tk:"#print " colGt "prefix" + cfg:(Lean.Parser.Tactic.config)? name:(ident)? : command => liftTermElabM do + if let some name := name then + let opts ← elabPrintPrefixConfig (mkOptionalNode cfg) + let mut msgs ← matchingConstants opts name.getId + if msgs.isEmpty then + if let [name] ← resolveGlobalConst name then + msgs ← matchingConstants opts name + logInfoAt tk (.joinSep msgs.toList "") diff --git a/test/print_prefix.lean b/test/print_prefix.lean index 77f89437c1..0d14e95aa3 100644 --- a/test/print_prefix.lean +++ b/test/print_prefix.lean @@ -171,3 +171,7 @@ TestInd.toCtorIdx : TestInd → Nat -/ #guard_msgs in #print prefix TestInd + +-- `#print prefix` does nothing if no identifier is provided +#guard_msgs in +#print prefix