fix: print prefix bug (#996)

Co-authored-by: Mario Carneiro <di.gama@gmail.com>
leanprover-community · Oct 19, 2024 · 1e0bf50 · 1e0bf50
1 parent 6f56968
commit 1e0bf50
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 9 deletions.
diff --git 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
@@ -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