refactor: add definitions to allow turnstiles anywhere in locations (#7425)

This PR adds definitions that will be required to allow to appear
turnstiles anywhere in tactic location specifiers.

This is the first (pre-stage0 update) half of #6992.

src/Init/Tactics.lean

@@ -461,10 +461,15 @@ syntax config := atomic(" (" &"config") " := " withoutPosition(term) ")"
 /-- The `*` location refers to all hypotheses and the goal. -/
 syntax locationWildcard := " *"
 
+/-- The `⊢` location refers to the current goal. -/
+syntax locationType := patternIgnore(atomic("|" noWs "-") <|> "⊢")
+
 /--
 A hypothesis location specification consists of 1 or more hypothesis references
 and optionally `⊢` denoting the goal.
 -/
+-- Forthcoming definition after stage0 update:
+-- syntax locationHyp := (ppSpace colGt (term:max <|> locationType))+
 syntax locationHyp := (ppSpace colGt term:max)+ patternIgnore(ppSpace (atomic("|" noWs "-") <|> "⊢"))?
 
 /--

src/Lean/Elab/Tactic/Location.lean

@@ -30,7 +30,14 @@ def expandLocation (stx : Syntax) : Location :=
   if arg.getKind == ``Parser.Tactic.locationWildcard then
     Location.wildcard
   else
-    Location.targets arg[0].getArgs (!arg[1].isNone)
+    -- Temporary workaround to accommodate stage0 update
+    if arg[1] matches .missing then
+      let locationHyps := arg[0].getArgs
+      let hypotheses := locationHyps.filter (·.getKind != ``Parser.Tactic.locationType)
+      let numTurnstiles := locationHyps.size - hypotheses.size
+      Location.targets hypotheses (numTurnstiles > 0)
+    else
+      Location.targets arg[0].getArgs (!arg[1].isNone)
 
 def expandOptLocation (stx : Syntax) : Location :=
   if stx.isNone then

src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;