fix: strict indentation check in · tacs

src/Init/NotationExtra.lean

@@ -376,9 +376,9 @@ section
 open Lean.Parser.Tactic
 syntax cdotTk := patternIgnore("· " <|> ". ")
 /-- `· tac` focuses on the main goal and tries to solve it using `tac`, or else fails. -/
-syntax cdotTk sepBy1IndentSemicolon(tactic) : tactic
+syntax cdotTk tacticSeqIndentGt : tactic
 macro_rules
-  | `(tactic| $cdot:cdotTk $tacs*) => `(tactic| {%$cdot $tacs* }%$cdot)
+  | `(tactic| $cdot:cdotTk $tacs) => `(tactic| {%$cdot ($tacs) }%$cdot)
 end
 
 /--

tests/lean/byStrictIndent.lean.expected.out

@@ -1,6 +1,6 @@
 theorem byTopLevelNoIndent : ∀ (n : Nat), n > 1 → n > 1 :=
 fun n h => h
-byStrictIndent.lean:12:2: error: expected '{' or strict indentation
+byStrictIndent.lean:12:2: error: expected '{' or indented tactic sequence
 byStrictIndent.lean:11:25-11:27: error: unsolved goals
 n : Nat
 h : n > 0

tests/lean/interactive/plainGoal.lean

@@ -128,3 +128,10 @@ example (hp : p) (hq : q) : p ∧ q := by
 example (hp : p) (hq : q) : p ∧ q :=
   show id (p ∧ q) by
                 --^ $/lean/plainGoal
+
+example : True ∧ False := by
+  constructor
+  · --
+ --^ $/lean/plainGoal
+  --^ $/lean/plainGoal
+  -- TODO: ^

tests/lean/interactive/plainGoal.lean.expected.out

@@ -164,3 +164,10 @@ null
  "position": {"line": 128, "character": 18}}
 {"rendered": "```lean\np q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)\n```",
  "goals": ["p q : Prop\nhp : p\nhq : q\n⊢ id (p ∧ q)"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 133, "character": 3}}
+{"rendered": "```lean\ncase left\n⊢ True\n```", "goals": ["case left\n⊢ True"]}
+{"textDocument": {"uri": "file://plainGoal.lean"},
+ "position": {"line": 133, "character": 4}}
+{"rendered": "```lean\ncase right\n⊢ False\n```",
+ "goals": ["case right\n⊢ False"]}