fix: trailing whitespace in location formatter (#3318)

This causes problems when used in conjunction with `#guard_msgs` (which
checks whitespace) and trailing whitespace removal. Discovered by
@PatrickMassot in verbose-lean4.

src/Init/Tactics.lean

@@ -398,7 +398,7 @@ syntax locationWildcard := " *"
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
-syntax locationHyp := (ppSpace colGt term:max)+ ppSpace patternIgnore( atomic("|" noWs "-") <|> "⊢")?
+syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
 
 /--
 Location specifications are used by many tactics that can operate on either the

tests/lean/formatTerm.lean

@@ -63,3 +63,5 @@ def foo : a b c d e f g a b c d e f g h where
 #eval fmt `(calc
   1 = 1 := rfl
   1 = 1 := rfl)
+
+#eval fmt `(by rw [] at h)

tests/lean/formatTerm.lean.expected.out

@@ -70,3 +70,4 @@ def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g
 calc
   1 = 1 := rfl✝
   1 = 1 := rfl✝
+by rw [] at h✝

tests/lean/simp_trace.lean.expected.out

@@ -65,7 +65,7 @@ Try this: simp only [bla, h] at *
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0
 [Meta.Tactic.simp.rewrite] unfold h, h x ==> Sum.inl (x, x)
-Try this: simp only [bla, h] at h' 
+Try this: simp only [bla, h] at h'
 [Meta.Tactic.simp.rewrite] unfold bla, bla x ==> match h x with
     | Sum.inl (y, z) => y + z
     | Sum.inr val => 0